proposition: Lemma addnA: forall (m n k : nat), m + (n + k) = (m + n) + k.
proof: Proof. Abort. Lemma addnA: forall (m n k : nat), m + (n + k) = m + n + k. Abort. Lemma addnA (m n k : nat) : m + (n + k) = m + n + k. Abort. Check 0 <= 4. Check (0 <= 4) = true. Check is_true . Check (_ <= _). Check is_true (_ <= _). Lemma leq0n (n : nat) : is_true (0 <= n). Abort. Lemma leq0n (n : nat) : 0 <= n. Abort. Print Nat.sub. Lemma eqn_leq (m n : nat) : m == n = (m <= n) && (n <= m). Abort. Lemma eqn_leq (m n : nat) : m == n = (m <= n <= m). Abort. Goal 2 + 2 = 4. Proof. by []. Qed.
imports: mathcomp(all_ssreflect)