proposition: Theorem Z_gcd_pos_r_le : ∀ a b, (Z.gcd a (Zpos b) <= Zpos b)%Z.
proof: Proof. intros a b. pose proof (Z.gcd_divide_r a (Zpos b)) as Hd. destruct Hd as (c, Hc). rewrite Hc in |- * at 2. rewrite Z.mul_comm. apply Z.le_mul_diag_r. pose proof (Z.gcd_nonneg a (Zpos b))%Z as H. assert (Z.gcd a (Zpos b) ≠ 0)%Z as HH. intros HH; apply Z.gcd_eq_0_r in HH. revert HH; apply Pos2Z_ne_0. lia. rename Hc into Hd. destruct (Z_zerop c) as [Hc| Hc]. subst c; simpl in Hd. exfalso; revert Hd; apply Pos2Z_ne_0. destruct c as [| c| c]. exfalso; apply Hc; reflexivity. pose proof (Pos2Z.is_pos c) as Hp. fast_omega Hp. exfalso; clear Hc. assert (Zpos b <= 0)%Z as HH. rewrite Hd. apply Z.mul_nonpos_nonneg. apply Pos2Z.neg_is_nonpos. apply Z.gcd_nonneg. apply Z.nlt_ge in HH. apply HH, Pos2Z.is_pos. Qed.
imports: Utf8 QArith NPeano Sorted Psatz