proposition: Lemma CNFr_ax_s f n: natp n -> CNFr_ax f (csucc n) -> CNFr_ax f n.
proof: Proof. move => nN [ax1 ax2]; move: (cltS nN) => pa;split=> //. by move=> i lin; apply: ax1; apply:clt_ltT lin pa. move => i iN si; apply: ax2 => //;apply:clt_ltT si pa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)