proposition: Lemma Z4_lt_is_transitive : forall x y z : Z4, Z4_lt x y -> Z4_lt y z -> Z4_lt x z.
proof: Proof. intros (((a, b), (c, d)), z4prf0) (((a', b'), (c', d')), z4prf1) (((a2, b2), (c2, d2)), z4prf2). unfold Z4_lt in |- *. unfold quadrointegral_lt in |- *. simpl in |- *. intros. apply Z.lt_trans with (a' + b' + c' + d')%Z; assumption. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)