proposition: Lemma csum_Mltlt a b c d : a <c b -> c <c d -> a +c c <c b +c d.
proof: Proof. move: a b c d. suff: forall a b c d, b <=c d -> a <c b -> c <c d -> a +c c <c b +c d. move => H a b c d le1 le2. move: (proj32_1 le1)(proj32_1 le2) => cb cd. case: (cleT_ee cb cd) => le3; first by apply: H. by rewrite (csumC a) (csumC b); apply: H. move => a b c d lebd lt1 lt2. case: (finite_or_infinite (proj32_1 lt2)). move /NatP => dN. exact: (csum_Mlelt (NS_le_nat lebd dN) (proj1 lt1) lt2). move => ifd. rewrite (csumC b) (csum_inf lebd ifd). exact: (csum_inf5 (clt_leT lt1 lebd) lt2 ifd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)