proposition: Lemma CNFb_r_ax e c n m: CNFb_ax e c n -> m <=c n -> CNFb_ax e c m.
proof: Proof. move => [p1 p2] mn; split; first by exact: (CNFq_r_ax p1 mn). move => i im; apply: p2; exact:(clt_leT im mn). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)