proposition: Lemma Z4_lt_is_irreflexive : forall x : Z4, ~ Z4_lt x x.
proof: Proof. intros (((a, b), (c, d)), z4prf0). unfold Z4_lt in |- *. unfold quadrointegral_lt in |- *. simpl in |- *. apply Z.lt_irrefl. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)