proposition: Lemma cnf_sum_prop3 x k : cnfp x -> k <=c domain x -> cnf_val (cnf_ns x k) +o cnf_val(cnf_nr x k) = cnf_val x.
proof: Proof. move => ha hb. move: (cnfp_cnf_nr ha hb) => hc. move: (cnfp_cnf_ns ha hb) => hd. by rewrite - {3} (cnfp_cnf_mergeK ha hb) - (cnf_sum_prop1 hc hd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)