proposition: Lemma cnf_le_prop x y: cnfp x -> cnfp y -> (forall e, Vr x e <=c Vr y e) -> x <=f y.
proof: Proof. move => ox oy h. case: (cnf_le_total ox oy) => // - [_ _ ]; case. by move ->; apply:cnf_leR. by move => [e /cltNge]; case; apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)