proposition: Lemma BigQfieldth : field_theory 0 1 BigQ.add BigQ.mul BigQ.sub BigQ.opp BigQ.div BigQ.inv BigQ.eq.
proof: Proof. constructor. exact BigQringth. exact BigQ.neq_1_0. exact BigQ.div_mul_inv. exact BigQ.mul_inv_diag_l. Qed.
imports: BigZ Field Qfield QSig QMake Orders GenericMinMax