def head_c

bend-collections-laws-math@1.0.0.0 · proofs/math/number/prime.bend:144

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

144def head_c(+n: Nat, +dq: Nat, +eq: Nat, +p: Nat, +hdd: {Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool}, +hs: {SN.nodiv(dq, n, 2n) == True{} : Bool}, +hde: {Nat.is_le(2n+dq, 2n+eq) == True{} : Bool}, +hek: {Nat.is_le(Nat.add(2n+eq, 1n+p), n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(Nat.mod(n, 2n+eq), 0n) == c : Bool}) -> {Bool.not(Nat.is_eq(Nat.mod(n, 2n+eq), 0n)) == True{} : Bool}:
145  match c:
146    case False{}:
147      %Equal.sym(Bool, Nat.is_eq(Nat.mod(n, 2n+eq), 0n), False{}, hc) : {Bool.not(_) == True{} : Bool}
148      {==}
149    case True{}:
150      +hm = N.eq_from_is_eq(Nat.mod(n, 2n+eq), 0n, hc)
151      +hn0 = R.dm_eq(1n+eq, n)
152      +hn1 = Equal.trans(Nat, n, Nat.add(Nat.mul(Nat.div(n, 2n+eq), 2n+eq), Nat.mod(n, 2n+eq)), Nat.mul(Nat.div(n, 2n+eq), 2n+eq), hn0, Equal.trans(Nat, Nat.add(Nat.mul(Nat.div(n, 2n+eq), 2n+eq), Nat.mod(n, 2n+eq)), Nat.add(Nat.mul(Nat.div(n, 2n+eq), 2n+eq), 0n), Nat.mul(Nat.div(n, 2n+eq), 2n+eq), Equal.cong(Nat, Nat, t => Nat.add(Nat.mul(Nat.div(n, 2n+eq), 2n+eq), t), Nat.mod(n, 2n+eq), 0n, hm), A.add_zero(Nat.mul(Nat.div(n, 2n+eq), 2n+eq))))
153      +hen = N.lt_le_trans(2n+eq, Nat.add(2n+eq, 1n+p), n, lt_add1(2n+eq, p), hek)
154      Empty.absurd({Bool.not(Nat.is_eq(Nat.mod(n, 2n+eq), 0n)) == True{} : Bool}, contra(n, dq, eq, Nat.div(n, 2n+eq), hn1, hen, hdd, hs, hde))