proposition: Lemma toto : forall a b q, S q * a = S q * b -> a = b.
proof: Proof. induction a. intros. rewrite Nat.mul_0_r in H. symmetry in H. apply Nat.eq_mul_0 in H. destruct H. discriminate H. auto. intros. destruct b. rewrite Nat.mul_0_r in H. discriminate H. assert (a=b). rewrite Nat.mul_succ_r in H. rewrite Nat.mul_succ_r in H. assert (S q + S q * a= S q + S q * b). rewrite Nat.add_comm. rewrite H. ring. apply Nat.add_cancel_l in H0. apply IHa with q. auto. rewrite H0. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)