proposition: Lemma isinjective_ne `{!IsInjective} x y : x <> y -> f x <> f y.
proof: Proof. intros E1 E2. apply E1. apply injective. assumption. Qed.
imports: Spaces.Nat.Core HoTT.Classes.interfaces.canonical_names Modalities.ReflectiveSubuniverse