diff --git a/theories/numbers.v b/theories/numbers.v index 56b1706a33572b91889e8e9a95c0e8319ebaf94c..df8c21a25c6b051cfb23e0d03af4a87ecad61e80 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -504,6 +504,8 @@ Infix "+" := Qp_plus : Qp_scope. Infix "-" := Qp_minus : Qp_scope. Infix "/" := Qp_div : Qp_scope. +Instance Qp_inhabited : Inhabited Qp := populate 1%Qp. + Lemma Qp_eq x y : x = y ↔ Qp_car x = Qp_car y. Proof. split; [by intros ->|].