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

@@ -860,7 +860,7 @@ Proof.
 Qed.
 
 Lemma Qp_plus_id_free q p : q + p = q → False.
-Proof. intro Heq. eapply (Qp_not_plus_ge q p). rewrite Heq. done. Qed.
+Proof. intro Heq. apply (Qp_not_plus_ge q p). by rewrite Heq.  Qed.
 
 Lemma Qp_plus_weak_r (q p o : Qp) : q + p ≤ o → q ≤ o.
 Proof. intros Le. eapply Qcle_trans; [ apply Qp_le_plus_l | apply Le ]. Qed.