(* DO NOT EDIT THIS FILE: automatically generated by ./gen_compare.sh *)
Require Import ZArith Floats.
Local Open Scope float_scope.

Definition min_denorm := Eval compute in ldexp one (-1074)%Z.

Definition min_norm := Eval compute in ldexp one (-1024)%Z.

Check (eq_refl false : nan =? nan = false).
Check (eq_refl false : nan =? nan = false).
Check (eq_refl false : nan <? nan = false).
Check (eq_refl false : nan <? nan = false).
Check (eq_refl false : nan <=? nan = false).
Check (eq_refl false : nan <=? nan = false).
Check (eq_refl FNotComparable : nan ?= nan = FNotComparable).
Check (eq_refl FNotComparable : nan ?= nan = FNotComparable).

Check (eq_refl false <: nan =? nan = false).
Check (eq_refl false <: nan =? nan = false).
Check (eq_refl false <: nan <? nan = false).
Check (eq_refl false <: nan <? nan = false).
Check (eq_refl false <: nan <=? nan = false).
Check (eq_refl false <: nan <=? nan = false).
Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable).
Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable).

Check (eq_refl false <<: nan =? nan = false).
Check (eq_refl false <<: nan =? nan = false).
Check (eq_refl false <<: nan <? nan = false).
Check (eq_refl false <<: nan <? nan = false).
Check (eq_refl false <<: nan <=? nan = false).
Check (eq_refl false <<: nan <=? nan = false).
Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable).
Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable).

Check (eq_refl false : nan =? - nan = false).
Check (eq_refl false : - nan =? nan = false).
Check (eq_refl false : nan <? - nan = false).
Check (eq_refl false : - nan <? nan = false).
Check (eq_refl false : nan <=? - nan = false).
Check (eq_refl false : - nan <=? nan = false).
Check (eq_refl FNotComparable : nan ?= - nan = FNotComparable).
Check (eq_refl FNotComparable : - nan ?= nan = FNotComparable).

Check (eq_refl false <: nan =? - nan = false).
Check (eq_refl false <: - nan =? nan = false).
Check (eq_refl false <: nan <? - nan = false).
Check (eq_refl false <: - nan <? nan = false).
Check (eq_refl false <: nan <=? - nan = false).
Check (eq_refl false <: - nan <=? nan = false).
Check (eq_refl FNotComparable <: nan ?= - nan = FNotComparable).
Check (eq_refl FNotComparable <: - nan ?= nan = FNotComparable).

Check (eq_refl false <<: nan =? - nan = false).
Check (eq_refl false <<: - nan =? nan = false).
Check (eq_refl false <<: nan <? - nan = false).
Check (eq_refl false <<: - nan <? nan = false).
Check (eq_refl false <<: nan <=? - nan = false).
Check (eq_refl false <<: - nan <=? nan = false).
Check (eq_refl FNotComparable <<: nan ?= - nan = FNotComparable).
Check (eq_refl FNotComparable <<: - nan ?= nan = FNotComparable).

Check (eq_refl true : one =? one = true).
Check (eq_refl true : one =? one = true).
Check (eq_refl false : one <? one = false).
Check (eq_refl false : one <? one = false).
Check (eq_refl true : one <=? one = true).
Check (eq_refl true : one <=? one = true).
Check (eq_refl FEq : one ?= one = FEq).
Check (eq_refl FEq : one ?= one = FEq).

Check (eq_refl true <: one =? one = true).
Check (eq_refl true <: one =? one = true).
Check (eq_refl false <: one <? one = false).
Check (eq_refl false <: one <? one = false).
Check (eq_refl true <: one <=? one = true).
Check (eq_refl true <: one <=? one = true).
Check (eq_refl FEq <: one ?= one = FEq).
Check (eq_refl FEq <: one ?= one = FEq).

Check (eq_refl true <<: one =? one = true).
Check (eq_refl true <<: one =? one = true).
Check (eq_refl false <<: one <? one = false).
Check (eq_refl false <<: one <? one = false).
Check (eq_refl true <<: one <=? one = true).
Check (eq_refl true <<: one <=? one = true).
Check (eq_refl FEq <<: one ?= one = FEq).
Check (eq_refl FEq <<: one ?= one = FEq).

Check (eq_refl true : zero =? zero = true).
Check (eq_refl true : zero =? zero = true).
Check (eq_refl false : zero <? zero = false).
Check (eq_refl false : zero <? zero = false).
Check (eq_refl true : zero <=? zero = true).
Check (eq_refl true : zero <=? zero = true).
Check (eq_refl FEq : zero ?= zero = FEq).
Check (eq_refl FEq : zero ?= zero = FEq).

Check (eq_refl true <: zero =? zero = true).
Check (eq_refl true <: zero =? zero = true).
Check (eq_refl false <: zero <? zero = false).
Check (eq_refl false <: zero <? zero = false).
Check (eq_refl true <: zero <=? zero = true).
Check (eq_refl true <: zero <=? zero = true).
Check (eq_refl FEq <: zero ?= zero = FEq).
Check (eq_refl FEq <: zero ?= zero = FEq).

Check (eq_refl true <<: zero =? zero = true).
Check (eq_refl true <<: zero =? zero = true).
Check (eq_refl false <<: zero <? zero = false).
Check (eq_refl false <<: zero <? zero = false).
Check (eq_refl true <<: zero <=? zero = true).
Check (eq_refl true <<: zero <=? zero = true).
Check (eq_refl FEq <<: zero ?= zero = FEq).
Check (eq_refl FEq <<: zero ?= zero = FEq).

Check (eq_refl true : zero =? - zero = true).
Check (eq_refl true : - zero =? zero = true).
Check (eq_refl false : zero <? - zero = false).
Check (eq_refl false : - zero <? zero = false).
Check (eq_refl true : zero <=? - zero = true).
Check (eq_refl true : - zero <=? zero = true).
Check (eq_refl FEq : zero ?= - zero = FEq).
Check (eq_refl FEq : - zero ?= zero = FEq).

Check (eq_refl true <: zero =? - zero = true).
Check (eq_refl true <: - zero =? zero = true).
Check (eq_refl false <: zero <? - zero = false).
Check (eq_refl false <: - zero <? zero = false).
Check (eq_refl true <: zero <=? - zero = true).
Check (eq_refl true <: - zero <=? zero = true).
Check (eq_refl FEq <: zero ?= - zero = FEq).
Check (eq_refl FEq <: - zero ?= zero = FEq).

Check (eq_refl true <<: zero =? - zero = true).
Check (eq_refl true <<: - zero =? zero = true).
Check (eq_refl false <<: zero <? - zero = false).
Check (eq_refl false <<: - zero <? zero = false).
Check (eq_refl true <<: zero <=? - zero = true).
Check (eq_refl true <<: - zero <=? zero = true).
Check (eq_refl FEq <<: zero ?= - zero = FEq).
Check (eq_refl FEq <<: - zero ?= zero = FEq).

Check (eq_refl true : - zero =? - zero = true).
Check (eq_refl true : - zero =? - zero = true).
Check (eq_refl false : - zero <? - zero = false).
Check (eq_refl false : - zero <? - zero = false).
Check (eq_refl true : - zero <=? - zero = true).
Check (eq_refl true : - zero <=? - zero = true).
Check (eq_refl FEq : - zero ?= - zero = FEq).
Check (eq_refl FEq : - zero ?= - zero = FEq).

Check (eq_refl true <: - zero =? - zero = true).
Check (eq_refl true <: - zero =? - zero = true).
Check (eq_refl false <: - zero <? - zero = false).
Check (eq_refl false <: - zero <? - zero = false).
Check (eq_refl true <: - zero <=? - zero = true).
Check (eq_refl true <: - zero <=? - zero = true).
Check (eq_refl FEq <: - zero ?= - zero = FEq).
Check (eq_refl FEq <: - zero ?= - zero = FEq).

Check (eq_refl true <<: - zero =? - zero = true).
Check (eq_refl true <<: - zero =? - zero = true).
Check (eq_refl false <<: - zero <? - zero = false).
Check (eq_refl false <<: - zero <? - zero = false).
Check (eq_refl true <<: - zero <=? - zero = true).
Check (eq_refl true <<: - zero <=? - zero = true).
Check (eq_refl FEq <<: - zero ?= - zero = FEq).
Check (eq_refl FEq <<: - zero ?= - zero = FEq).

Check (eq_refl true : infinity =? infinity = true).
Check (eq_refl true : infinity =? infinity = true).
Check (eq_refl false : infinity <? infinity = false).
Check (eq_refl false : infinity <? infinity = false).
Check (eq_refl true : infinity <=? infinity = true).
Check (eq_refl true : infinity <=? infinity = true).
Check (eq_refl FEq : infinity ?= infinity = FEq).
Check (eq_refl FEq : infinity ?= infinity = FEq).

Check (eq_refl true <: infinity =? infinity = true).
Check (eq_refl true <: infinity =? infinity = true).
Check (eq_refl false <: infinity <? infinity = false).
Check (eq_refl false <: infinity <? infinity = false).
Check (eq_refl true <: infinity <=? infinity = true).
Check (eq_refl true <: infinity <=? infinity = true).
Check (eq_refl FEq <: infinity ?= infinity = FEq).
Check (eq_refl FEq <: infinity ?= infinity = FEq).

Check (eq_refl true <<: infinity =? infinity = true).
Check (eq_refl true <<: infinity =? infinity = true).
Check (eq_refl false <<: infinity <? infinity = false).
Check (eq_refl false <<: infinity <? infinity = false).
Check (eq_refl true <<: infinity <=? infinity = true).
Check (eq_refl true <<: infinity <=? infinity = true).
Check (eq_refl FEq <<: infinity ?= infinity = FEq).
Check (eq_refl FEq <<: infinity ?= infinity = FEq).

Check (eq_refl true : - infinity =? - infinity = true).
Check (eq_refl true : - infinity =? - infinity = true).
Check (eq_refl false : - infinity <? - infinity = false).
Check (eq_refl false : - infinity <? - infinity = false).
Check (eq_refl true : - infinity <=? - infinity = true).
Check (eq_refl true : - infinity <=? - infinity = true).
Check (eq_refl FEq : - infinity ?= - infinity = FEq).
Check (eq_refl FEq : - infinity ?= - infinity = FEq).

Check (eq_refl true <: - infinity =? - infinity = true).
Check (eq_refl true <: - infinity =? - infinity = true).
Check (eq_refl false <: - infinity <? - infinity = false).
Check (eq_refl false <: - infinity <? - infinity = false).
Check (eq_refl true <: - infinity <=? - infinity = true).
Check (eq_refl true <: - infinity <=? - infinity = true).
Check (eq_refl FEq <: - infinity ?= - infinity = FEq).
Check (eq_refl FEq <: - infinity ?= - infinity = FEq).

Check (eq_refl true <<: - infinity =? - infinity = true).
Check (eq_refl true <<: - infinity =? - infinity = true).
Check (eq_refl false <<: - infinity <? - infinity = false).
Check (eq_refl false <<: - infinity <? - infinity = false).
Check (eq_refl true <<: - infinity <=? - infinity = true).
Check (eq_refl true <<: - infinity <=? - infinity = true).
Check (eq_refl FEq <<: - infinity ?= - infinity = FEq).
Check (eq_refl FEq <<: - infinity ?= - infinity = FEq).

Check (eq_refl false : min_denorm =? min_norm = false).
Check (eq_refl false : min_norm =? min_denorm = false).
Check (eq_refl true : min_denorm <? min_norm = true).
Check (eq_refl false : min_norm <? min_denorm = false).
Check (eq_refl true : min_denorm <=? min_norm = true).
Check (eq_refl false : min_norm <=? min_denorm = false).
Check (eq_refl FLt : min_denorm ?= min_norm = FLt).
Check (eq_refl FGt : min_norm ?= min_denorm = FGt).

Check (eq_refl false <: min_denorm =? min_norm = false).
Check (eq_refl false <: min_norm =? min_denorm = false).
Check (eq_refl true <: min_denorm <? min_norm = true).
Check (eq_refl false <: min_norm <? min_denorm = false).
Check (eq_refl true <: min_denorm <=? min_norm = true).
Check (eq_refl false <: min_norm <=? min_denorm = false).
Check (eq_refl FLt <: min_denorm ?= min_norm = FLt).
Check (eq_refl FGt <: min_norm ?= min_denorm = FGt).

Check (eq_refl false <<: min_denorm =? min_norm = false).
Check (eq_refl false <<: min_norm =? min_denorm = false).
Check (eq_refl true <<: min_denorm <? min_norm = true).
Check (eq_refl false <<: min_norm <? min_denorm = false).
Check (eq_refl true <<: min_denorm <=? min_norm = true).
Check (eq_refl false <<: min_norm <=? min_denorm = false).
Check (eq_refl FLt <<: min_denorm ?= min_norm = FLt).
Check (eq_refl FGt <<: min_norm ?= min_denorm = FGt).

Check (eq_refl false : min_denorm =? one = false).
Check (eq_refl false : one =? min_denorm = false).
Check (eq_refl true : min_denorm <? one = true).
Check (eq_refl false : one <? min_denorm = false).
Check (eq_refl true : min_denorm <=? one = true).
Check (eq_refl false : one <=? min_denorm = false).
Check (eq_refl FLt : min_denorm ?= one = FLt).
Check (eq_refl FGt : one ?= min_denorm = FGt).

Check (eq_refl false <: min_denorm =? one = false).
Check (eq_refl false <: one =? min_denorm = false).
Check (eq_refl true <: min_denorm <? one = true).
Check (eq_refl false <: one <? min_denorm = false).
Check (eq_refl true <: min_denorm <=? one = true).
Check (eq_refl false <: one <=? min_denorm = false).
Check (eq_refl FLt <: min_denorm ?= one = FLt).
Check (eq_refl FGt <: one ?= min_denorm = FGt).

Check (eq_refl false <<: min_denorm =? one = false).
Check (eq_refl false <<: one =? min_denorm = false).
Check (eq_refl true <<: min_denorm <? one = true).
Check (eq_refl false <<: one <? min_denorm = false).
Check (eq_refl true <<: min_denorm <=? one = true).
Check (eq_refl false <<: one <=? min_denorm = false).
Check (eq_refl FLt <<: min_denorm ?= one = FLt).
Check (eq_refl FGt <<: one ?= min_denorm = FGt).

Check (eq_refl false : min_norm =? one = false).
Check (eq_refl false : one =? min_norm = false).
Check (eq_refl true : min_norm <? one = true).
Check (eq_refl false : one <? min_norm = false).
Check (eq_refl true : min_norm <=? one = true).
Check (eq_refl false : one <=? min_norm = false).
Check (eq_refl FLt : min_norm ?= one = FLt).
Check (eq_refl FGt : one ?= min_norm = FGt).

Check (eq_refl false <: min_norm =? one = false).
Check (eq_refl false <: one =? min_norm = false).
Check (eq_refl true <: min_norm <? one = true).
Check (eq_refl false <: one <? min_norm = false).
Check (eq_refl true <: min_norm <=? one = true).
Check (eq_refl false <: one <=? min_norm = false).
Check (eq_refl FLt <: min_norm ?= one = FLt).
Check (eq_refl FGt <: one ?= min_norm = FGt).

Check (eq_refl false <<: min_norm =? one = false).
Check (eq_refl false <<: one =? min_norm = false).
Check (eq_refl true <<: min_norm <? one = true).
Check (eq_refl false <<: one <? min_norm = false).
Check (eq_refl true <<: min_norm <=? one = true).
Check (eq_refl false <<: one <=? min_norm = false).
Check (eq_refl FLt <<: min_norm ?= one = FLt).
Check (eq_refl FGt <<: one ?= min_norm = FGt).

Check (eq_refl false : one =? infinity = false).
Check (eq_refl false : infinity =? one = false).
Check (eq_refl true : one <? infinity = true).
Check (eq_refl false : infinity <? one = false).
Check (eq_refl true : one <=? infinity = true).
Check (eq_refl false : infinity <=? one = false).
Check (eq_refl FLt : one ?= infinity = FLt).
Check (eq_refl FGt : infinity ?= one = FGt).

Check (eq_refl false <: one =? infinity = false).
Check (eq_refl false <: infinity =? one = false).
Check (eq_refl true <: one <? infinity = true).
Check (eq_refl false <: infinity <? one = false).
Check (eq_refl true <: one <=? infinity = true).
Check (eq_refl false <: infinity <=? one = false).
Check (eq_refl FLt <: one ?= infinity = FLt).
Check (eq_refl FGt <: infinity ?= one = FGt).

Check (eq_refl false <<: one =? infinity = false).
Check (eq_refl false <<: infinity =? one = false).
Check (eq_refl true <<: one <? infinity = true).
Check (eq_refl false <<: infinity <? one = false).
Check (eq_refl true <<: one <=? infinity = true).
Check (eq_refl false <<: infinity <=? one = false).
Check (eq_refl FLt <<: one ?= infinity = FLt).
Check (eq_refl FGt <<: infinity ?= one = FGt).

Check (eq_refl false : - infinity =? infinity = false).
Check (eq_refl false : infinity =? - infinity = false).
Check (eq_refl true : - infinity <? infinity = true).
Check (eq_refl false : infinity <? - infinity = false).
Check (eq_refl true : - infinity <=? infinity = true).
Check (eq_refl false : infinity <=? - infinity = false).
Check (eq_refl FLt : - infinity ?= infinity = FLt).
Check (eq_refl FGt : infinity ?= - infinity = FGt).

Check (eq_refl false <: - infinity =? infinity = false).
Check (eq_refl false <: infinity =? - infinity = false).
Check (eq_refl true <: - infinity <? infinity = true).
Check (eq_refl false <: infinity <? - infinity = false).
Check (eq_refl true <: - infinity <=? infinity = true).
Check (eq_refl false <: infinity <=? - infinity = false).
Check (eq_refl FLt <: - infinity ?= infinity = FLt).
Check (eq_refl FGt <: infinity ?= - infinity = FGt).

Check (eq_refl false <<: - infinity =? infinity = false).
Check (eq_refl false <<: infinity =? - infinity = false).
Check (eq_refl true <<: - infinity <? infinity = true).
Check (eq_refl false <<: infinity <? - infinity = false).
Check (eq_refl true <<: - infinity <=? infinity = true).
Check (eq_refl false <<: infinity <=? - infinity = false).
Check (eq_refl FLt <<: - infinity ?= infinity = FLt).
Check (eq_refl FGt <<: infinity ?= - infinity = FGt).

Check (eq_refl false : - infinity =? one = false).
Check (eq_refl false : one =? - infinity = false).
Check (eq_refl true : - infinity <? one = true).
Check (eq_refl false : one <? - infinity = false).
Check (eq_refl true : - infinity <=? one = true).
Check (eq_refl false : one <=? - infinity = false).
Check (eq_refl FLt : - infinity ?= one = FLt).
Check (eq_refl FGt : one ?= - infinity = FGt).

Check (eq_refl false <: - infinity =? one = false).
Check (eq_refl false <: one =? - infinity = false).
Check (eq_refl true <: - infinity <? one = true).
Check (eq_refl false <: one <? - infinity = false).
Check (eq_refl true <: - infinity <=? one = true).
Check (eq_refl false <: one <=? - infinity = false).
Check (eq_refl FLt <: - infinity ?= one = FLt).
Check (eq_refl FGt <: one ?= - infinity = FGt).

Check (eq_refl false <<: - infinity =? one = false).
Check (eq_refl false <<: one =? - infinity = false).
Check (eq_refl true <<: - infinity <? one = true).
Check (eq_refl false <<: one <? - infinity = false).
Check (eq_refl true <<: - infinity <=? one = true).
Check (eq_refl false <<: one <=? - infinity = false).
Check (eq_refl FLt <<: - infinity ?= one = FLt).
Check (eq_refl FGt <<: one ?= - infinity = FGt).