proposition: Lemma cnf_compare_nat_sum5 x y z: cnfp x -> cnfp y -> cnfp z -> (x +#f z <=f y +#f z <-> x <=f y).
proof: Proof. move => ox oy oz. have H: forall a b, a <f b -> a +#f z <f b +#f z. clear x y ox oy => a b [[oa ob etc] nab]; case: etc => // - [e ea eb]. apply/(cnf_lt_prop (cnfp_nat_sum oa oz)(cnfp_nat_sum ob oz)). exists e. rewrite (cnf_nat_sum_p2 oa oz) (cnf_nat_sum_p2 ob oz). exact: (csum_Mlteq (NS_Vr e oz) ea). by move => e' h; rewrite (cnf_nat_sum_p2 oa oz) (cnf_nat_sum_p2 ob oz) eb. have tv: x +#f z <=f x +#f z by apply: (cnf_leR (cnfp_nat_sum ox oz)). case: (cnf_le_total ox oy) => lxy; split. - exact. - move => _; case: (equal_or_not x y) => exy; first by rewrite - exy. exact: (proj1 (H _ _ (conj lxy exy))). - move => l1; case: (equal_or_not y x) => exy; first by move: lxy; rewrite exy. by move: (H _ _ (conj lxy exy)) => [ra]; case; apply: (cnf_leA). - by move =>h; rewrite (cnf_leA lxy h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)