diff --git a/prelude/numbers.v b/prelude/numbers.v index 50d60a0da3e354f8eda5e9190c496d5d126f15eb..2a410297acff4e4e2806531f15bffc6ccf6e0887 100644 --- a/prelude/numbers.v +++ b/prelude/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 ->|].