Skip to content
Snippets Groups Projects
Commit 94a98b3f authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Change eapply to apply

parent e3d278f8
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/numbers.v
+ 1
− 1
View file @ 94a98b3f
......@@ -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.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment