proposition: Lemma gtx_mult_compat : forall m m' n n', m >_0 m' -> n >>= n' -> m * n >_0 m' * n'.
proof: Proof. intros. destruct m; destruct m'; destruct n; destruct n'; destruct H; destruct H0; simpl; try solve [ exfalso; auto | intuition; discr | left; simpl; auto | left; simpl in *; lia | right; auto ]. left. simpl. injection H0. intro. subst n. simpl in H. lia. Qed.
imports: CoLoR(AArcticBasedInt Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil NatUtil AWFMInterpretation LogicUtil AMatrixBasedInt BoolUtil ListUtil)