proposition: Lemma Z8_lt_is_well_def_rht : is_well_def_rht Z8 Z8_lt Z8_eq.
proof: Proof. red in |- *. intros ((((a, b), (c, d)), ((e, f), (g, h))), z8prf0) ((((a', b'), (c', d')), ((e', f'), (g', h'))), z8prf1). intro H. intros ((((a2, b2), (c2, d2)), ((e2, f2), (g2, h2))), z8prf2). generalize H. unfold Z8_lt in |- *. unfold Z8_eq in |- *. unfold octointegral_lt in |- *. unfold octointegral_eq in |- *. simpl in |- *. clear H z8prf0 z8prf1 z8prf2. intros H0 (H1, (H2, (H3, (H4, (H5, (H6, (H7, H8))))))). repeat match goal with | id:(?X1 = ?X2) |- _ => try rewrite id in H0; clear id end. assumption. Qed.
imports: QArithSternBrocot(Merge_Order)