proposition: Lemma Rabs_div : forall a b : R, b <> 0 -> Rabs (a/b) = (Rabs a) / (Rabs b).
proof: Proof. intros. unfold Rdiv. rewrite Rabs_mult. rewrite Rabs_Rinv. reflexivity. apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)