Lemma NQmax_eq_zero : ∏ x y : NonnegativeRationals, NQmax x y = 0 -> (x = 0) × (y = 0). Proof. intros x y. unfold NQmax. generalize (isdecrel_leNonnegativeRationals x y). apply (coprod_rect (λ _, _ → _)) ; [ intros Hle | intros Hlt] ; intro H ; simpl in H ; split. - apply NonnegativeRationals_eq0_le0. apply istrans_leNonnegativeRationals with (1 := Hle). now rewrite H ; apply isrefl_leNonnegativeRationals. - exact H. - exact H. - apply NonnegativeRationals_eq0_le0 ; rewrite <- H. now apply lt_leNonnegativeRationals, notge_ltNonnegativeRationals. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.Fields. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim.