proposition: Lemma Pplus_one_succ_r p : Pos.succ p = p + 1.
proof: Proof. Proof (eq_sym (Pos.add_1_r p)). Lemma Pplus_one_succ_l p : Pos.succ p = 1 + p. Proof (eq_sym (Pos.add_1_l p)). Lemma Pcompare_refl p : Pos.compare_cont Eq p p = Eq. Proof (Pos.compare_cont_refl p Eq). Lemma Pcompare_Eq_eq : forall p q, Pos.compare_cont Eq p q = Eq -> p = q. Proof Pos.compare_eq. Lemma ZC4 p q : Pos.compare_cont Eq p q = CompOpp (Pos.compare_cont Eq q p). Proof (Pos.compare_antisym q p). Lemma Ppred_minus p : Pos.pred p = p - 1. Proof (eq_sym (Pos.sub_1_r p)). Lemma Pminus_mask_Gt p q : p > q -> exists h : positive, Pos.sub_mask p q = IsPos h /\ q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = IsPos (Pos.pred h)). Proof. intros H. apply Pos.gt_lt in H. destruct (Pos.sub_mask_pos p q H) as (r & U). exists r. repeat split; trivial. - now apply Pos.sub_mask_pos_iff. - destruct (Pos.eq_dec r 1) as [EQ|NE]; [now left|right]. rewrite Pos.sub_mask_carry_spec, U. destruct r; trivial. now elim NE. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef