proposition: Lemma Z_to_Qmult_POS_NEG : forall p1 p2 : positive, Z_to_Q (Zpos p1 * Zneg p2) = Qmult (Z_to_Q (Zpos p1)) (Z_to_Q (Zneg p2)).
proof: Proof. intros p1 p2. unfold Z_to_Q at 2 3 in |- *. unfold Qmult in |- *. replace (Zpos p1 * Zneg p2)%Z with (Zneg (p1 * p2)); trivial. unfold Z_to_Q at 1 in |- *. apply f_equal with Qpositive. unfold Qpositive_mult in |- *. repeat rewrite Qpositive_i_c. repeat rewrite Nat.mul_1_l. apply f_equal3 with nat nat nat; trivial. apply nat_of_P_mult_morphism. rewrite nat_of_P_mult_morphism. lia. apply lt_O_nat_of_P. constructor. apply lt_O_nat_of_P. constructor. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)