proposition: Lemma length_last : forall x l, length (l & x) = 1 + length l.
proof: Proof. Proof using. intros. unfold length. rew_list~. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)