def ones4_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbits.bend:64

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

64def ones4_eq(+n: Nat, +h: {Nat.is_lt(n, 16n) == True{} : Bool}) -> {F.ones4(n) == SN.ones(4n, n) : Nat}:
65  match n:
66    case 0n:
67      {==}
68    case 1n:
69      {==}
70    case 2n:
71      {==}
72    case 3n:
73      {==}
74    case 4n:
75      {==}
76    case 5n:
77      {==}
78    case 6n:
79      {==}
80    case 7n:
81      {==}
82    case 8n:
83      {==}
84    case 9n:
85      {==}
86    case 10n:
87      {==}
88    case 11n:
89      {==}
90    case 12n:
91      {==}
92    case 13n:
93      {==}
94    case 14n:
95      {==}
96    case 15n:
97      {==}
98    case 16n+m:
99      Empty.absurd({F.ones4(16n+m) == SN.ones(4n, 16n+m) : Nat}, N.lt_zero_absurd(m, h))