proposition: Lemma compare_sum_prod0 a b : \2c <=c a -> \2c <=c b -> a +c b <=c a *c b.
proof: Proof. move => ag2 bg2. rewrite -(cdiff_pr ag2) cprodDl - csumA - csum_nn; set c := _ -c _. rewrite - csumA (csumC _ b); apply:(csum_Mlele bg2). apply:csum_Meqle. exact:(cprod_M1le (CS_diff a \2c) (nesym(proj2(clt_leT clt_02 bg2)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)