proposition: Lemma cons_to_app: forall {T: Type}(ls: list T)(e: T), e :: ls = [e] ++ ls.
proof: Proof. intros. assert (A := app_nil_l ls). rewrite <- A at 1. rewrite app_comm_cons. reflexivity. Qed.
imports: Coq(Bool Arith Arith.Peano_dec Arith.Compare_dec List)