proposition: Lemma exercice6_2 a b c d: a <c c -> b <c d -> ((a +c b) <c (c +c d) /\ (a *c b) <c (c *c d)).
proof: Proof. move=> ac bd. wlog: a b c d ac bd / ( c <=c d). move=> h. case: (cleT_ee (proj32_1 ac) (proj32_1 bd)) => aux. by apply: h. by rewrite csumC (csumC c _) cprodC (cprodC c _); apply: h. move=> cd. have cnz: c <> \0c. move=> cz; rewrite cz in ac; exact: (clt0 ac). have cad:= proj32 cd. case: (finite_or_infinite cad) => fcd. move: ac => [ac _]. have dN: natp d by apply /NatP. have bN:= NS_lt_nat bd dN. have cN:= NS_le_nat cd dN. have aN:= NS_le_nat ac cN. split; [ apply: csum_Mlelt => // | apply: cprod_Mlelt => //]. rewrite (cprodC c d) (csumC c d). rewrite (cprod_inf cd fcd cnz) (csum_inf cd fcd). have caa:= proj31_1 ac. have cab:= proj31_1 bd. have fcz:= finite_0. wlog : / (infinite_c b /\ a <=c b); last first. move=> [fcb leab]. split; first by rewrite csumC (csum_inf leab fcb). rewrite cprodC; case: (equal_or_not a \0c) => az. by rewrite az cprod0r; apply: clt_fin_inf. by rewrite (cprod_inf leab fcb az). move=> wwlog; case: (finite_or_infinite caa) => fca. case: (finite_or_infinite cab) => fcb. split; apply: clt_fin_inf => //; fprops. move: (cle_fin_inf fca fcb) => ab; apply: wwlog;split => //. case: (cleT_ee caa cab) => ba. case: (finite_or_infinite cab) => fcb. case: (cleNgt ba (clt_fin_inf fcb fca)). apply: wwlog;split => //. have ltad:= clt_leT ac cd. split; first by rewrite (csum_inf ba fca). case: (equal_or_not b \0c) => bz. by rewrite bz cprod0r; apply: clt_fin_inf. by rewrite (cprod_inf ba fca bz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)