proposition: Lemma pos_sub_add p q r : pos_sub (p + q) r = pos p + pos_sub q r.
proof: Proof. simpl. rewrite !pos_sub_spec. case (Pos.compare_spec q r); intros E0. - subst. assert (H := Pos.lt_add_r r p). rewrite Pos.add_comm in H. apply Pos.lt_gt in H. now rewrite H, Pos.add_sub. - rewrite pos_sub_spec. assert (Hr : (r = (r-q)+q)%positive) by (now rewrite Pos.sub_add). rewrite Hr at 1. rewrite Pos.add_compare_mono_r. case Pos.compare_spec; intros E1; trivial; f_equal. + rewrite Pos.add_comm. apply Pos.sub_add_distr. rewrite Hr, Pos.add_comm. now apply Pos.add_lt_mono_r. + symmetry. apply Pos.sub_sub_distr; trivial. - assert (LT : (r < p + q)%positive). { apply Pos.lt_trans with q; trivial. rewrite Pos.add_comm. apply Pos.lt_add_r. } apply Pos.lt_gt in LT. rewrite LT. f_equal. symmetry. now apply Pos.add_sub_assoc. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass