proposition: Lemma cnf_leA x y: x <=f y -> y <=f x -> x = y.
proof: Proof. move => [ox oy la ][_ _ lb]; case: la => // - [e ea eb]. case: lb => // - [i ia ib]. have H a b: a <c b -> b <> \0o. move => h; exact: (nesym (proj2 (cle_ltT (cle0x (proj31_1 h)) h))). move: (Vr_ne2 oy (H _ _ ea)) (Vr_ne2 ox (H _ _ ia)). move => oe oi; case: (oleT_ell oe oi) => h. - by rewrite h in ea ia; case: (proj2 (clt_ltT ea ia)). - by case: (proj2 ia); rewrite (eb _ h). - by case: (proj2 ea); rewrite (ib _ h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)