proposition: Lemma cnf_sum_prop10 x y: cnfp x -> cnfp_nz y -> ~(inc (cnf_degree y) (domain (range x))) -> cnf_sum_compat x y.
proof: Proof. move => ox ynz hd. rewrite/cnf_sum_compat (cnf_sum_prop9 ox ynz hd). move: (OS_cnf_degree ynz) => od. move: (position_in_cnf_prop ox od) =>[kdx kp1 kp2]. move:(cnfp_cnf_ns ox kdx) (cnfp_cnf_nr ox kdx) => ox1 ox2. rewrite (cnf_sum_prop1 (proj1 ynz) ox1) - (cnf_sum_prop3 ox kdx). rewrite - (osumA (OS_cnf_val ox1) (OS_cnf_val ox2) (OS_cnf_val (proj1 ynz))). apply: f_equal. symmetry; apply: (ord_negl_p9 ox ynz kdx kp1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)