proposition: Lemma strong_injective_preserves_0 : (forall x, x ≶ 0 -> f x ≶ 0) -> IsStrongInjective f.
proof: Proof. intros E1. split; try apply _. intros x y E2. apply (strong_extensionality (+ -f y)). rewrite plus_negate_r, <-preserves_minus. apply E1. apply (strong_extensionality (+ y)). rewrite <-simple_associativity,left_inverse,plus_0_l,plus_0_r. trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.apartness HoTT.Classes.theory.rings