proposition: Lemma lem_rev_lst {A} : forall l : list A, rev l = List.rev l.
proof: Proof. unfold rev. induction l; sauto use: @lem_itrev. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation