proposition: Lemma cnf_lt_prop x y: cnfp x -> cnfp y -> (x <f y <-> cnf_lt1 x y).
proof: Proof. move => ox oy; split. by move => [[_ _ ha] hb]; case: ha. move => ha; split; first by split => //; right. by move => exy; case: ha=> d /proj2 b _; case: b; rewrite exy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)