fact: Definition Z4_eq (x y : Z4) := let (V1, V2) := z4crr x in let (V3, V4) := z4crr y in let (a, b) := V1 in let (c, d) := V2 in let (a', b') := V3 in let (c', d') := V4 in quadrointegral_eq a b c d a' b' c' d'.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)