theorem-proving - リーンで帰納法によって証明を単純化する方法は?

Question

リーンの帰納法による証明を簡単にしたいと思います。

リーンで 3 つのコンストラクターを持つ誘導型を定義し、この型のバイナリ関係を定義しました。Lean では公理を rel のコンストラクタとして使用できないため、公理を含めました。

inductive Fintype : Type
| a : Fintype
| b : Fintype
| c : Fintype

inductive rel : Fintype → Fintype →  Prop 
| r1 : rel Fintype.a Fintype.b
| r2 : ∀ p : Prop, (p → rel Fintype.a Fintype.c )
| r3 : ∀ p : Prop, (¬ p → rel Fintype.c Fintype.b) 


axiom asymmetry_for_Fintype : ∀ x y : Fintype, rel x y → ¬ rel y x
axiom trivial1 : ¬ rel Fintype.c Fintype.a
axiom trivial2 : ¬ rel Fintype.b Fintype.c
axiom trivial3 : ∀ p : Prop, rel Fintype.a Fintype.c → p 
axiom trivial4 : ∀ p : Prop, rel Fintype.c Fintype.b → ¬ p

目標は、次の定理を証明することでした。

def nw_o_2 (X : Type) (binrel : X → X → Prop) (x y : X) : Prop := ¬ binrel y x
def pw_o_2 (X : Type) (binrel : X → X → Prop )(x y : X) : Prop := ∀ z : X, (binrel z x → binrel z y) ∧ (binrel y z → binrel x z)

theorem simple17: ∀ x y : Fintype, nw_o_2 Fintype rel x y → pw_o_2 Fintype rel x y :=

x、y、z の帰納法によって証明しました。「z」は、上記の pw_o_2 の定義に由来します。しかし、証明は非常に長い (~136 行)。より短い証明を持つ別の方法はありますか？