(forall x, x ≶ 0 -> f x ≶ 0) -> IsStrongInjective f. 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.
Require Import