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