proposition: Lemma Dle_df_correct : forall x : float10, forall y : float2, Dle_df x y = true -> (x <= y)%R.
proof: Proof. intros x y H. apply Rcompare_not_Lt_inv. revert H. unfold Dle_df. rewrite Dcompare_correct. now case Rcompare. Qed.
imports: Flocq.Core.Defs Gappa_common