proposition: Lemma cprod_increasing0 I (f g: fterm): (forall x, inc x I -> f x <=c g x) -> (cprodb I f) <=c (cprodb I g).
proof: Proof. move=> ale; apply:cprod_increasing; aw; trivial => i idx. by rewrite !LgV //; apply: ale. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)