proposition: Lemma CNFq_p4 e c n i: CNFb_ax e c n -> i <c n -> \0o <o cantor_mon e c i.
proof: Proof. move => [[pa pb pc pd] pe] lin. apply: oprod2_pos; last by exact(pe _ lin). exact:(opow_pos (olt_leT (olt_02) pa) (pb _ lin)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)