proposition: Lemma image_false : forall f domain y, image f domain y = false -> forall x, x < domain -> f x = y -> False.
proof: Proof. intros f dom; induction dom; intros y T x Bx Exy. inversion Bx. simpl in T. auto_if; dumb. apply (IHdom y T x); dumb. cut (x <> dom); dumb. Qed.
imports: ZArith Lia MyNat