proposition: Lemma add_right_S : forall (n m : nat), S (add_right n m) = add_right (S n) m.
proof: Proof. intros. autoinduct on (add_right n m) || (idtac "step0 test4 fails"; induction m). all: (simpl; congruence). Qed.
imports: Autoinduct(Autoinduct)