proposition: Lemma Z4_lt_is_well_def_rht : is_well_def_rht Z4 Z4_lt Z4_eq.
proof: Proof. red in |- *. intros (((a, b), (c, d)), z4prf0) (((a', b'), (c', d')), z4prf1). intro H. intros (((a2, b2), (c2, d2)), z4prf2). generalize H. unfold Z4_lt in |- *. unfold Z4_eq in |- *. unfold quadrointegral_lt in |- *. unfold quadrointegral_eq in |- *. simpl in |- *. clear H z4prf0 z4prf1 z4prf2. intros H0 (H1, (H2, (H3, H4))). repeat match goal with | id:(?X1 = ?X2) |- _ => try rewrite id in H0; clear id end. assumption. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)