proposition: Lemma Z8_eq_is_reflexive : forall x : Z8, Z8_eq x x.
proof: Proof. intros ((((a, b), (c, d)), ((e, f), (g, h))), z8prf0). unfold Z8_eq in |- *. unfold octointegral_eq in |- *; repeat split. Qed.
imports: QArithSternBrocot(Merge_Order)