Repository navigation

Add lemmas and definitions from Alethe development - #74

Merged

fblanqui merged 13 commits into

Deducteam:masterfrom

NotBad4U:add-lemmas

Oct 2, 2026

Merged

Add lemmas and definitions from Alethe development#74
fblanqui merged 13 commits into
Deducteam:masterfrom
NotBad4U:add-lemmas

Commits on Sep 29, 2026
- Add lemmas and definitions from Alethe development
  NotBad4U
  committed
  ada38d0
- Fix all comment of PR review
  NotBad4U
  committed
  3e45885
- Update mergesort and fix coprod deps
  NotBad4U
  committed
  360919a
Commits on Oct 1, 2026
- remove useless require
  fblanqui
  committed
  16d8eb7
- CHANGES: record only changes wrt previous release
  fblanqui
  committed
  c35c950
- remove useless requires
  fblanqui
  committed
  02cef9a
- remove useless explicit arguments
  fblanqui
  committed
  32041cc
- moved relation between sum and prod at the end
  fblanqui
  committed
  7afda8c
- derive ProdExt by defining Prod inductively
  fblanqui
  committed
  42735f1
- update CHANGES
  fblanqui
  committed
  2b684cb
Commits on Oct 2, 2026
- details
  fblanqui
  committed
  8f293f1
- details
  fblanqui
  committed
  c8a10c5
- details
  fblanqui
  committed
  496c0fa