proposition: Lemma strong_injective_preserves_0 : (∀ x, x ≶ 0 → f x ≶ 0) → StrongInjective 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)). now ring_simplify. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.strong_setoids MathClasses.theory.rings