def internal_length_odds_le

bend-mathlib@0.8.1.0 · sort.bend:205

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

205def internal_length_odds_le(~A: Data, +xs: List<&2, A>) -> {Nat.is_le(List.length(&2, A, MPerm.odds(A, xs)), List.length(&2, A, xs)) == True{} : Bool}:
206  match xs:
207    case Nil{}:
208      {==}
209    case +x <> +r:
210      match r:
211        case Nil{}:
212          {==}
213        case +y <> +t:
214          MNat.succ_le_succ(List.length(&2, A, MPerm.odds(A, t)), 1n+List.length(&2, A, t), MNat.le_trans(List.length(&2, A, MPerm.odds(A, t)), List.length(&2, A, t), 1n+List.length(&2, A, t), internal_length_odds_le(~A, t), MNat.le_succ(List.length(&2, A, t))))