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