proposition: Lemma Qinv_mult_distr : forall p q, / (p * q) == /p * /q.
proof: Proof. intros (x1,x2) (y1,y2); unfold Qeq, Qinv, Qmult; simpl. destruct x1; simpl; auto; destruct y1; simpl; auto. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool