def internal_length_evens_le

bend-mathlib@0.8.1.0 · sort.bend:194

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat
import bend-mathlib@0.8.1.0/perm.bend as MPerm

194def internal_length_evens_le(~A: Data, +xs: List<&2, A>) -> {Nat.is_le(List.length(&2, A, MPerm.evens(A, xs)), List.length(&2, A, xs)) == True{} : Bool}:
195  match xs:
196    case Nil{}:
197      {==}
198    case +x <> +r:
199      match r:
200        case Nil{}:
201          {==}
202        case +y <> +t:
203          MNat.succ_le_succ(List.length(&2, A, MPerm.evens(A, t)), 1n+List.length(&2, A, t), MNat.le_trans(List.length(&2, A, MPerm.evens(A, t)), List.length(&2, A, t), 1n+List.length(&2, A, t), internal_length_evens_le(~A, t), MNat.le_succ(List.length(&2, A, t))))