proposition: Lemma BigQringth : ring_theory 0 1 BigQ.add BigQ.mul BigQ.sub BigQ.opp BigQ.eq.
proof: Proof. constructor. exact BigQ.add_0_l. exact BigQ.add_comm. exact BigQ.add_assoc. exact BigQ.mul_1_l. exact BigQ.mul_comm. exact BigQ.mul_assoc. exact BigQ.mul_add_distr_r. exact BigQ.sub_add_opp. exact BigQ.add_opp_diag_r. Qed.
imports: BigZ Field Qfield QSig QMake Orders GenericMinMax