proposition: Lemma Zmult_compat : forall n m, 0<=n -> 0<n*m -> 0<n /\ 0<m.
proof: Proof. intros. case (Z_lt_le_dec 0 n). intros H'. replace 0 with (0*n) in H0 by ring; replace (n*m) with (m*n) in H0 by ring; generalize (Zmult_gt_0_lt_reg_r _ _ _ (Z.lt_gt _ _ H') H0);auto. intro; assert (n=0) by lia. subst;simpl in H0. lia. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)