proposition: Theorem Zplus_mod_one: forall a1 b1, 0 < b1 -> (a1 + b1) mod b1 = a1 mod b1.
proof: Proof. intros a1 b1 H; rewrite Zplus_mod by zarith. rewrite Z_mod_same by zarith; rewrite Z.add_0_r. apply Zmod_mod; auto. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase