proposition: Lemma Z4_eq_is_transitive : forall x y z : Z4, Z4_eq x y -> Z4_eq y z -> Z4_eq x z.
proof: Proof. intros (((a, b), (c, d)), z4prf0) (((a', b'), (c', d')), z4prf1) (((a2, b2), (c2, d2)), z4prf2). unfold Z4_eq in |- *. unfold quadrointegral_eq in |- *. simpl in |- *. intros (HH2, (HH4, (HH6, HH7))) (HH9, (HH11, (HH13, HH14))); repeat split; match goal with | id12:(?X1 = ?X2),id23:(?X2 = ?X3) |- (?X1 = ?X3) => try apply (trans_eq id12 id23) end. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)