proposition: Theorem Qeq_shift_mult_l : ∀ x y z, ¬z == 0 → x / z == y → x == y * z.
proof: Proof. intros x y z Hc H. rewrite <- H. rewrite Qmult_div_swap. rewrite Qdiv_mult_l; [ reflexivity | assumption ]. Qed.
imports: Utf8 QArith NPeano Sorted Psatz