proposition: Lemma mult_same_l : forall n3 n1 n2, n3 > 0 -> n3 * n1 = n3 * n2 -> n1 = n2.
proof: Proof. intuition. eapply mult_same_r; eauto. rewrite Nat.mul_comm. rewrite (Nat.mul_comm n2 n3). trivial. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat