Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/coqtokyo_question_0927_without_ssreflect.v

Created September 27, 2022 07:10
Show Gist options
  • Save yoshihiro503/95f7ea4b941e55681b3ceb1c37d47fe3 to your computer and use it in GitHub Desktop.
Save yoshihiro503/95f7ea4b941e55681b3ceb1c37d47fe3 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
coqtokyo_question_0927_without_ssreflect.v
Require Import Arith.
Lemma test_000: forall a b c : nat, a + b + c = b + c + a.
Proof.
intros a b c. now rewrite (Nat.add_comm a b), Nat.add_shuffle0.
Qed.
Lemma test_001: forall m : nat, 2 ^ (S m) = 2 * 2 ^ m.
Proof. reflexivity. Qed.
Lemma test_002: forall a b c : nat, a * b ^ c = b ^ c * a.
Proof.
intros a b c. now apply Nat.mul_comm.
Qed.
Lemma test_003: forall a b c : nat, a * b ^ c / a = b ^ c * a / a.
Proof.
intros a b c. now rewrite Nat.mul_comm.
Qed.
Lemma test_004: forall a b c : nat, a + b ^ c = b ^ c + a.
Proof.
intros a b c. now rewrite Nat.add_comm.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment