proposition: Lemma spec_Qquadratic_Qpositive_to_Q_commut : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), spec_Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 = spec_Qquadratic_Qpositive_to_Q a c b d e g f h p2 p1.
proof: Proof. intros a b c d e f g h p1 p2. unfold spec_Qquadratic_Qpositive_to_Q in |- *. abstract (apply f_equal2 with Q Q; solve [ ring | apply f_equal with Q; ring ]). Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)