proposition: Lemma add_right_comm: forall (n m : nat), add_right n m = add_right m n.
proof: Proof. intros. autoinduct on add_right || (idtac "step1 test6 fails"; induction m). all: simpl. - symmetry. apply add_right_O. - (rewrite IHm || rewrite IHn0). apply add_right_S. Qed.
imports: Autoinduct(Autoinduct)