proposition: Lemma Rabs_idem : forall x : R, (x <= Rabs x)%R.
proof: Proof. intro x. unfold Rabs. case Rcase_abs ; intro H. apply Rle_trans with (1 := (Rlt_le _ _ H)). auto with real. apply Req_le. apply refl_equal. Qed.
imports: Gappa_common Gappa_decimal