proposition: Lemma mult_same_r : forall n1 n2 n3, n3 > 0 -> n1 * n3 = n2 * n3 -> n1 = n2.
proof: Proof. induction n1; destruct n2; intuition idtac; simpl in *. remember (n2 * n3) as x. lia. remember (n1 * n3) as x. lia. f_equal. eapply IHn1; eauto. eapply Nat.add_cancel_l. eauto. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat