proposition: Lemma Z4_eq_is_symmetric : forall x y : Z4, Z4_eq x y -> Z4_eq y x.
proof: Proof. intros (((a, b), (c, d)), z4prf0) (((a', b'), (c', d')), z4prf1). unfold Z4_eq in |- *. unfold quadrointegral_eq in |- *. intros (HH1, (HH2, (HH3, HH4))); repeat split; symmetry in |- *; assumption. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)