proposition: Lemma image_injective_plus_one : forall domain f, same (image f (S domain)) (union (image f domain) (singleton (f domain))).
proof: Proof. intros dom f i. unfold union, singleton. simpl; auto_if; auto with *. Qed.
imports: ZArith Lia MyNat