proposition: Lemma length_zero_eq_eq_nil : forall l, (length l = 0) = (l = nil).
proof: Proof. Proof using. intros. unfolds length. rewrite <-LibList.length_zero_eq_eq_nil. math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)