proposition: Lemma cnf_rem_prop1 x: cnfp x -> cnf_rem x = cnf_val (cnf_nr x (cnf_size x)).
proof: Proof. move => /proj42 / NS_pred ha. rewrite /cnf_rem /cnf_val /cnf_nr restr_d; apply: (osumf_exten ha). by move => i iln; rewrite/cantor_mon /oexp /ocoef LgV//; apply/NltP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)