Definition maponcomplincl_ne {X Y : UU} (f : X -> Y) (is : isincl f) (x : X) (neq_x : neqPred x) (neq_fx : neqPred (f x)) : compl_ne X x neq_x -> compl_ne Y (f x) neq_fx. Proof. intros c. set (x' := pr1 c). set (neqx := pr2 c). exact (f x',,neg_to_negProp (nP := neq_fx (f x')) (negf (invmaponpathsincl _ is x x') (negProp_to_neg neqx))). Defined.