proposition: Theorem Rabs_gt : forall x y, (y < -x \/ x < y)%R -> (x < Rabs y)%R.
proof: Proof. intros x y [Hyx|Hxy]. rewrite <- Rabs_Ropp. apply Rlt_le_trans with (Ropp y). apply Ropp_lt_cancel. now rewrite Ropp_involutive. apply RRle_abs. apply Rlt_le_trans with (1 := Hxy). apply RRle_abs. Qed.
imports: Coq(Psatz Reals ZArith) Zaux