proposition: Lemma diveucl_21_spec_aux : forall a1 a2 b, wB/2 <= φ b -> φ a1 < φ b -> let (q,r) := diveucl_21 a1 a2 b in φ a1 *wB+ φ a2 = φ q * φ b + φ r /\ 0 <= φ r < φ b.
proof: Proof. intros a1 a2 b H1 H2;assert (W:= diveucl_21_spec a1 a2 b). assert (W1:= to_Z_bounded a1). assert (W2:= to_Z_bounded a2). assert (Wb:= to_Z_bounded b). assert (φ b>0) as H by (auto with zarith). generalize (Z_div_mod (φ a1*wB+φ a2) φ b H). revert W. destruct (diveucl_21 a1 a2 b); destruct (Z.div_eucl (φ a1*wB+φ a2) φ b). intros (H', H''); auto; rewrite H', H''; clear H' H''. intros (H', H''); split; [ |exact H'']. now rewrite H', Zmult_comm. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63