proposition: Lemma Eq_mul_mon2 a b c: b <=s c -> a \times b <=s a \times c.
proof: Proof. move => [f [[ff fi] sf tf]]. exists (Lf (fun t => J (P t) (Vf f (Q t))) (a \times b) (a \times c));saw. apply: lf_injective. move => t /setX_P [_ ha ]; rewrite - sf => /(Vf_target ff); rewrite tf => h. by apply setXp_i. move => u v /setX_P [pu ha hb] /setX_P [pv cb hd] /pr12_def [eq1 eq2]. apply: (pair_exten pu pv eq1); apply: fi; try ue. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)