proposition: Lemma lem_rev_rev {A} : forall l : list A, rev (rev l) = l.
proof: Proof. unfold rev. induction l as [| x l IH]. - reflexivity. - sauto use: (lem_itrev l [x]), (lem_rev_app (itrev l []) [x]). Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation