proposition: Lemma mod_le_2r : forall (a b r: positive) (q:N), Zpos a = b*q + r -> b <= a -> r < b -> 2*r <= a.
proof: Proof. intros a b r q H0 H1 H2. assert (H3:=Zlt_0_pos a). assert (H4:=Zlt_0_pos b). assert (H5:=Zlt_0_pos r). destruct q as [|q]. rewrite Zmult_0_r in H0. exfalso;lia. assert (H6:=Zlt_0_pos q). unfold Z_of_N in H0. assert (Zpos r = a - b*q). lia. simpl;zsimpl. pattern r at 2;rewrite H. assert (b <= b * q). pattern (Zpos b) at 1;rewrite <- (Zmult_1_r b). apply Zmult_le_compat;try lia. apply Z.le_trans with (a - b * q + b). lia. apply Z.le_trans with (a - b + b);lia. Qed.
imports: ZArith Lia ZCmisc