proposition: Lemma intransitive1pr : let intransitive_alt:= forall x y z t, x <> y -> x <> z -> x <> t -> y <> z -> y <> t -> z <> t -> inc x E -> inc y E -> inc z E -> inc t E -> R x y -> R x z -> R x t -> R y z -> R y t -> R z t in intransitive1 <-> intransitive_alt.
proof: Proof. rewrite /intransitive1; split. move=> h x y z t H0 _ _ _ _ _ _ _ _ _ H10 H11 H12 H13 H14. apply: (h x y z t H0 H10 H11 H12 H13 H14). move=> h x y z t nxy xy xz xt yz yt. move: (A3 xy) (A3 yz)(A3 (A2 xz))(A3 (A2 yt)) => xE yE sE tE. case: (equal_or_not x z) => nxz; first by ue. case: (equal_or_not x t) => nxt; first by apply: A2; ue. case: (equal_or_not y z) => nyz; first by ue. case: (equal_or_not y t) => nyt; first by apply: A2; ue. case: (equal_or_not z t)=> nzt; first by rewrite nzt -A1. apply: (h x y z t) =>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)