proposition: Lemma sg_tuple_equal : forall (l1 a1 b1 c1 d1 : Z) (p1 : Qpositive) (l2 a2 b2 c2 d2 : Z) (p2 : Qpositive), (l1, (a1, (b1, (c1, d1)), p1)) = (l2, (a2, (b2, (c2, d2)), p2)) -> l1 = l2 /\ (a1 = a2 /\ b1 = b2 /\ c1 = c2 /\ d1 = d2) /\ p1 = p2.
proof: Proof. intros. inversion H; (repeat split; reflexivity). Qed.
imports: Coq(ZArithRing) QArithSternBrocot(Zaux)