Add Qp lemmas

Adds a two additional lemmas for Qp.

Also renames a few lemmas that accidentally had Qc in their name instead of Qp. These where introduced back in !179 (merged) so it's probably safe to assume that no one are using the misnamed ones.

theories/numbers.v

@@ -838,9 +838,6 @@ Proof.
   apply Hle, Qp_prf.
 Qed.
 
-Lemma Qp_not_plus_q_ge_1 (q: Qp) : ¬ (1 + q)%Qp ≤ 1%Qp.
-Proof. apply Qp_not_plus_ge. Qed.
-
 Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc.
 Proof. apply Qclt_le_weak, Qp_prf. Qed.