proposition: Lemma CNFq_r_ax e c n m: CNFq_ax e c n -> m <=c n -> CNFq_ax e c m.
proof: Proof. move => [p1 p2 p3 p4] mn; split. + done. + move => i im; apply: p2;exact: (clt_leT im mn). + move => i im; apply: p3;exact: (clt_leT im mn). + move => i iN im; apply: p4 => //; exact(clt_leT im mn). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)