proposition: Theorem iter_com: forall (A B : Set) zero (f : A -> A -> B) g l1 l2, (forall a, g a zero = a) -> (forall a b c, g a (g b c) = g (g a b) c) -> (forall a b, g a b = g b a) -> iter zero (fun x => iter zero (fun y => f x y) g l1) g l2 = iter zero (fun y => iter zero (fun x => f x y) g l2) g l1.
proof: Proof. intros A B zero f g l1 l2 H H0 H1; generalize l2; elim l1; simpl; auto; clear l1 l2. intros l2; elim l2; simpl; auto with arith. intros; rewrite H1; rewrite H; auto with arith. intros a l1 H2 l2; case l2; clear l2; simpl; auto. elim l1; simpl; auto with arith. intros; rewrite H1; rewrite H; auto with arith. intros b l2. rewrite <- (iter_comp _ _ zero (fun x => f x a) (fun x => iter zero (fun (y : A) => f x y) g l1)); auto with arith. rewrite <- (iter_comp _ _ zero (fun y => f b y) (fun y => iter zero (fun (x : A) => f x y) g l2)); auto with arith. (repeat rewrite H0); auto. apply f_equal2 with ( f := g ); auto. (repeat rewrite <- H0); auto. apply f_equal2 with ( f := g ); auto. Qed.
imports: List Permutation Arith