proposition: Lemma cnf_leT x y z: x <=f y -> y <=f z -> x <=f z.
proof: Proof. move => lexy leyz; move: (leyz) => [oy oz];case; [by move <- | move => lyz]. move: lexy =>[ox _];case; [by move -> | move => [e ea eb] ]. move: lyz => [i ia ib]. have H a b: a <c b -> b <> \0o. move => h; exact: (nesym (proj2 (cle_ltT (cle0x (proj31_1 h)) h))). split => //; right. move: (Vr_ne2 oy (H _ _ ea)) (Vr_ne2 oz (H _ _ ia)). move => oe oi; case: (oleT_ell oe oi) => h. - exists e; first by apply: (clt_ltT ea); rewrite h. by move => j jle; rewrite eb // ib // -h . - exists i; first by rewrite eb. by move => j lj; rewrite - ib // eb //; apply: (olt_ltT h lj). - exists e; first by rewrite - ib. by move => j lj; rewrite eb // ib //; apply: (olt_ltT h lj). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)