proposition: Lemma Cab_trans a b x y: a<> b -> R a b -> intransitive1 -> x<> y -> inc x (Cab a b) -> inc y (Cab a b) -> (Cab a b)= (Cab x y).
proof: Proof. move=> nab rab i1 nxy /Zo_P [xE [r1 r2]] /Zo_P [yE [r3 r4]]. set_extens t; move /Zo_P=> [tE [r5 r6]]; apply/Zo_i => //; split. - apply: (i1 a b x t) =>//. - apply: (i1 a b y t) =>//; apply: A2. - apply: (i1 x y a t) =>//; first apply: (i1 a b x y)=>//; apply: A2=> //. - apply: (i1 x y b t) =>//; first apply: (i1 a b x y)=>//; apply: A2=> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)