proposition: Lemma cnf_nat_sum_p3 x y z : cnfp x -> cnfp y -> cnfp z -> (forall e, Vr z e = (Vr x e) +c Vr y e) -> z = x +#f y.
proof: Proof. move => ox oy oz hz. move:(cnfp_nat_sum ox oy) (cnf_nat_sum_p2 ox oy); set t := cnf_nat_sum x y. move => ot tp. by apply:(Vr_exten oz ot) => e; rewrite tp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)