proposition: Lemma cnf_sum_prop2 x y: cnfp x -> cnfp y -> cnf_all_smaller x y -> cnf_sum_compat y x.
proof: Proof. move => ha hb hc; by rewrite /cnf_sum_compat - (cnf_nm_sum ha hb hc) (cnf_sum_prop1 ha hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)