proposition: Lemma Z8_lt_is_irreflexive : forall x : Z8, ~ Z8_lt x x.
proof: Proof. intros ((((a, b), (c, d)), ((e, f), (g, h))), z8prf0). unfold Z8_lt in |- *. unfold octointegral_lt in |- *. simpl in |- *. apply Z.lt_irrefl. Qed.
imports: QArithSternBrocot(Merge_Order)