proposition: Lemma cnf_sumA x y z: cnfp x -> cnfp y -> cnfp z -> x +f (y +f z) = (x +f y) +f z.
proof: Proof. move => ox oy oz. move: (cnfp_sum oy oz) (cnfp_sum ox oy) => oyz oxy. apply: (cnf_val_inj (cnfp_sum ox oyz) (cnfp_sum oxy oz)). rewrite (cnf_sum_compat_prop ox oyz) (cnf_sum_compat_prop oxy oz). rewrite (cnf_sum_compat_prop oy oz)(cnf_sum_compat_prop ox oy). exact: (osumA (OS_cnf_val ox)(OS_cnf_val oy)(OS_cnf_val oz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)