proposition: Lemma abs_length : forall i l, i = length l -> abs i = LibList.length l.
proof: Proof. Proof using. introv E. unfold length in E. applys eq_nat_of_eq_int. rewrite abs_nonneg; math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)