Code

Rebase changes from earlier Cauchy PR#21

Code

Merged

palmskog merged 2 commits intomastercoq-community/dedekind-reals:masterfrom cauchycoq-community/dedekind-reals:cauchyCopy head branch name to clipboardJul 14, 2024

+629-482

Commits

Commits on Jul 14, 2024

• Prove that the lift of negated disjunctions is enough to merge Cauchy and Dedekind reals

  

  VincentSe

  authored and

  palmskog

  committed
  7723a8d

  Copy full SHA for 7723a8d

• convert Cauchy.v and DecOrder.v to Unix newlines

  palmskog

  committed
  481d4d7

  Copy full SHA for 481d4d7