proposition: Lemma cnf_sum_compat_prop x y: cnfp x -> cnfp y -> cnf_sum_compat x y.
proof: Proof. move => ox oy. have oox := OS_cnf_val ox. case: (equal_or_not y emptyset) => ynz. by rewrite /cnf_sum_compat ynz cnf_sum0r cnf_val0 (osum0r oox). case: (inc_or_not (cnf_degree y)(domain (range x))). move/funI_P => [p /(range_gP (proj41 ox)) [k kdx kv] pv]. move/(NltP (proj42 ox)): (kdx) => lkx. have hu: oexp x k = cnf_degree y by rewrite pv/oexp - kv. exact: (cnf_sum_prop7 ox (conj oy ynz) lkx hu). exact: cnf_sum_prop10. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)