Skip to content

Remove lemmas addP and mulP #35

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
vbgl merged 1 commit into from
Nov 6, 2025
Merged

Remove lemmas addP and mulP #35

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 2 additions & 9 deletions src/word_ssrZ.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@

(* -------------------------------------------------------------------- *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint intdiv.

Check warning on line 25 in src/word_ssrZ.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20) 

Notations "\pi ( _ )" defined at level 2 and "\pi"

Check warning on line 25 in src/word_ssrZ.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20) 

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
From Coq Require Import Arith ZArith.

Set Implicit Arguments.
Expand Down Expand Up @@ -50,13 +50,6 @@
Qed.
End PosInd.

(* -------------------------------------------------------------------- *)
Lemma addP m n : (m + n)%coq_nat = (m + n)%nat.
Proof. by []. Qed.

Lemma mulP m n : (m * n)%coq_nat = (m * n)%nat.
Proof. by []. Qed.

(* -------------------------------------------------------------------- *)
Definition int_to_Z (z : int) : Z :=
match z with
Expand Down Expand Up @@ -244,10 +237,10 @@
split=> // -[|x|x] y /=; first by rewrite mul0r.
- elim/posind: x => [|p ih]; first by rewrite !mul1r.
rewrite Pos2Z.inj_add addZE mulrDl mul1r raddfD /=.
by rewrite ih Pos2Nat.inj_add /= addP PoszD mulrDl mul1r.
by rewrite ih Pos2Nat.inj_add /= PoszD mulrDl mul1r.
- elim/posind: x => [|p ih]; first by rewrite !mulN1r raddfN.
rewrite -Pos2Z.add_neg_neg addZE mulrDl mulN1r.
rewrite raddfB /= ih Pos2Nat.inj_add addP PoszD.
rewrite raddfB /= ih Pos2Nat.inj_add PoszD.
by rewrite opprD mulrDl mulN1r.
Qed.

Expand Down
Loading