Skip to content
Snippets Groups Projects
Commit 2891ec49 authored by François Bobot's avatar François Bobot
Browse files

[Coq] Remove a SearchAbout

parent 4ba8aea9
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
lib/coq/for_drivers/ComputerOfEuclideanDivision.v
+ 0
− 1
View file @ 2891ec49
...@@ -64,7 +64,6 @@ Lemma cmod_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z -> ...@@ -64,7 +64,6 @@ Lemma cmod_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
(-d)%Z))%Z))))). (-d)%Z))%Z))))).
intros n d. intros n d.
unfold int.EuclideanDivision.mod1. unfold int.EuclideanDivision.mod1.
SearchAbout Z.rem Z.quot.
assert (Z.rem n d = n - (d * (Z.quot n d)))%Z. assert (Z.rem n d = n - (d * (Z.quot n d)))%Z.
assert (H:= Z.quot_rem' n d). assert (H:= Z.quot_rem' n d).
omega. omega.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment