proposition: Lemma length_app : forall l1 l2, length (l1 ++ l2) = length l1 + length l2.
proof: Proof. Proof using. intros. unfold length at 1. rewrite fold_right_app. fold (length l2). induction l1; rew_listx. { auto. } { rewrite length_cons. rewrite IHl1. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)