proposition: Lemma Cab_stable a b: a<> b -> R a b -> intransitive1 -> stableR (Cab a b).
proof: Proof. move=> nab Rab i1; rewrite /Cab=> u v. move /Zo_P=> [_ [r1 r2]] /Zo_P [_ [r3 r4]]; apply: (i1 a b u v) =>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)