proposition: Lemma Z8_eq_is_transitive : forall x y z : Z8, Z8_eq x y -> Z8_eq y z -> Z8_eq x z.
proof: Proof. intros ((((a, b), (c, d)), ((e, f), (g, h))), z8prf0) ((((a', b'), (c', d')), ((e', f'), (g', h'))), z8prf1) ((((a2, b2), (c2, d2)), ((e2, f2), (g2, h2))), z8prf2). unfold Z8_eq in |- *. unfold octointegral_eq in |- *. simpl in |- *. clear z8prf0 z8prf1 z8prf2. intros (H1, (H2, (H3, (H4, (H5, (H6, (H7, H8))))))) (H9, (H10, (H11, (H12, (H13, (H14, (H15, H16))))))); repeat split; match goal with | id12:(?X1 = ?X2),id23:(?X2 = ?X3) |- (?X1 = ?X3) => try apply (trans_eq id12 id23) end. Qed.
imports: QArithSternBrocot(Merge_Order)