tchajed/strong-induction
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
Proof of strong induction in Coq
2 commits 1 branch 0 tags 28 KiB
  • Rocq Prover 100%
Find a file
Exact
Tej Chajed 6203a12301
 Add a basic README
2016-12-04 15:20:49 -05:00
.gitignore Initial version of strong induction principle 2016-12-04 15:13:49 -05:00
README.md Add a basic README 2016-12-04 15:20:49 -05:00
StrongInduction.v Initial version of strong induction principle 2016-12-04 15:13:49 -05:00

README.md

Strong induction

StrongInduction.v proves the principle of strong induction over natural numbers:

Theorem strong_induction : forall P : nat -> Prop,
  (forall m : nat, (forall n : nat, n < m -> P n) -> P m) ->
  forall n : nat, P n.