proposition: Lemma image_false_pr f dom y : (forall i, i < dom -> y <> f i) -> image f dom y = false.
proof: Proof. intros NE. remember (image f dom y) as b; symmetry in Heqb. destruct b; [ exfalso | reflexivity ]. destruct (image_true _ _ _ Heqb) as (n, Hn). specialize (NE n); intuition. Qed.
imports: ZArith Lia MyNat