proposition: Lemma NQmax_eq_zero : ∏ x y : NonnegativeRationals, NQmax x y = 0 -> (x = 0) × (y = 0).
proof: 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.
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.RealNumbers.Sets UniMath.RealNumbers.Fields UniMath.Algebra.DivisionRig UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim