def internal_nat_le_total

bend-mathlib@0.8.1.0 · order.bend:87

import Base

87# Nat calls of the laws above: --verdict takes a ~ constant's model from a call of its law (PLAN F38).
88def internal_nat_le_total(a: Nat, b: Nat) -> {Bool.or(Nat.is_le(a, b), Nat.is_le(b, a)) == True{} : Bool}:
89  match a b:
90    case 0n 0n:
91      {==}
92    case 0n 1n+q:
93      {==}
94    case 1n+p 0n:
95      {==}
96    case 1n+p 1n+q:
97      internal_nat_le_total(p, q)