proposition: Lemma cnf_nat_sum_p1 x y : cnfp x -> cnfp y -> cnf_exponents (x +#f y) = cnf_exponents x \cup cnf_exponents y.
proof: Proof. move => ox oy. move:(cnf_sort_correct (cnf_nat_sum_range ox oy)). set z := cnf_sort _; move => [za zb]. rewrite {1}/cnf_exponents zb /cnf_nat_sum_mons; set_extens t. by move/funI_P =>[a /funI_P[b bE ->] ->]; rewrite pr1_pair. move=> jE; apply/funI_P. exists ( J t (Vr x t +c Vr y t)); last by aw. apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)