proposition: Lemma Z8_eq_is_symmetric : forall x y : Z8, Z8_eq x y -> Z8_eq y x.
proof: Proof. intros ((((a, b), (c, d)), ((e, f), (g, h))), z8prf0) ((((a', b'), (c', d')), ((e', f'), (g', h'))), z8prf1). unfold Z8_eq in |- *. unfold octointegral_eq in |- *. intros (H1, (H2, (H3, (H4, (H5, (H6, (H7, H8))))))); repeat split; symmetry in |- *; assumption. Qed.
imports: QArithSternBrocot(Merge_Order)