Verified Commit 17190de7 authored by Tej Chajed's avatar Tej Chajed
Browse files

Use coqdoc syntax

parent 0210d4c9
Pipeline #58441 passed with stage
in 4 minutes and 23 seconds
......@@ -65,10 +65,10 @@ Proof. unfold lt. apply _. Qed.
Lemma nat_le_sum (x y : nat) : x y z, y = x + z.
Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
(* [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
(** [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
Lemma nat_minus_plus n m : n + m - n = m.
Proof. lia. Qed.
(* [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
(** [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
Lemma nat_le_plus_minus n m : n m m = n + (m - n).
Proof. lia. Qed.
......
Supports Markdown
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