proposition: Lemma Rabs_eq_0 : forall x, Rabs x = 0 -> x = 0.
proof: Proof. intros. unfold Rabs in H. destruct Rcase_abs. rewrite <- (Ropp_involutive x). apply Ropp_eq_0_compat. apply H. apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)