proposition: Lemma Z8_lt_is_transitive : forall x y z : Z8, Z8_lt x y -> Z8_lt y z -> Z8_lt 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_lt in |- *. unfold octointegral_lt in |- *. simpl in |- *. intros. apply Z.lt_trans with (a' + b' + c' + d' + e' + f' + g' + h')%Z; assumption. Qed.
imports: QArithSternBrocot(Merge_Order)