diff --git a/theories/numbers.v b/theories/numbers.v index f577584944a857ee2a9c3e8f0658e90a89796b97..7a1cfcc87304ab096a2fd47925862485e7046eaa 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -47,6 +47,8 @@ Instance S_inj: Inj (=) (=) S. Proof. by injection 1. Qed. Instance nat_le_po: PartialOrder (≤). Proof. repeat split; repeat intro; auto with lia. Qed. +Instance nat_le_total: Total (≤). +Proof. repeat intro; lia. Qed. Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y). Proof. @@ -145,6 +147,9 @@ Instance positive_le_dec: RelDecision Pos.le. Proof. refine (λ x y, decide ((x ?= y) ≠ Gt)). Defined. Instance positive_lt_dec: RelDecision Pos.lt. Proof. refine (λ x y, decide ((x ?= y) = Lt)). Defined. +Instance positive_le_total: Total Pos.le. +Proof. repeat intro; lia. Qed. + Instance positive_inhabited: Inhabited positive := populate 1. Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end. @@ -320,6 +325,9 @@ Instance N_le_po: PartialOrder (≤)%N. Proof. repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm. Qed. +Instance N_le_total: Total (≤)%N. +Proof. repeat intro; lia. Qed. + Hint Extern 0 (_ ≤ _)%N => reflexivity : core. (** * Notations and properties of [Z] *) @@ -363,6 +371,8 @@ Instance Z_le_po : PartialOrder (≤). Proof. repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm. Qed. +Instance Z_le_total: Total Z.le. +Proof. repeat intro; lia. Qed. Lemma Z_pow_pred_r n m : 0 < m → n * n ^ (Z.pred m) = n ^ m. Proof. @@ -496,14 +506,17 @@ Next Obligation. intros x y; apply Qcle_not_lt. Qed. Instance Qc_lt_pi x y : ProofIrrel (x < y). Proof. unfold Qclt. apply _. Qed. -Instance: PartialOrder (≤). +Instance Qc_le_po: PartialOrder (≤). Proof. repeat split; red. apply Qcle_refl. apply Qcle_trans. apply Qcle_antisym. Qed. -Instance: StrictOrder (<). +Instance Qc_lt_strict: StrictOrder (<). Proof. split; red. intros x Hx. by destruct (Qclt_not_eq x x). apply Qclt_trans. Qed. +Instance Qc_le_total: Total Qcle. +Proof. intros x y. destruct (Qclt_le_dec x y); auto using Qclt_le_weak. Qed. + Lemma Qcmult_0_l x : 0 * x = 0. Proof. ring. Qed. Lemma Qcmult_0_r x : x * 0 = 0.