proposition: Theorem permutation_rev: forall (A:Set) (l : list A), permutation (rev l) l.
proof: Proof. intros a l; elim l; simpl; auto. intros a1 l1 Hl1. apply permutation_trans with (cons a1 (rev l1)); [|auto]. change (permutation (rev l1 ++ (a1 :: nil)) (app (cons a1 nil) (rev l1))); auto. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression