proposition: Lemma Ndiv_mult_simpl : forall a b q, q <> 0 -> (a * q | b * q) -> (a | b).
proof: Proof. intros. destruct H0. destruct q. contradiction H. reflexivity. rewrite Nat.mul_assoc in H0. assert (S q*b=S q*(q0*a)). rewrite Nat.mul_comm. rewrite H0. ring. assert (b=q0*a). apply toto with q. rewrite Nat.mul_comm. rewrite H0. ring. apply Ndivide_intro with q0. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)