proposition: Lemma add_le_r m n: if (n <=? m + n)%uint63 then (φ m + φ n < wB)%Z else (wB <= φ m + φ n)%Z.
proof: Proof. case (to_Z_bounded m); intros H1m H2m. case (to_Z_bounded n); intros H1n H2n. case (Zle_or_lt wB (φ m + φ n)); intros H. - assert (H1: (φ (m + n) = φ m + φ n - wB)%Z). { rewrite add_spec. replace ((φ m + φ n) mod wB)%Z with ((((φ m + φ n) - wB) + wB) mod wB)%Z. - rewrite -> Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith. rewrite !Zmod_small; auto with zarith. - apply (f_equal2 Z.modulo); auto with zarith. } case_eq (n <=? m + n)%uint63; auto. rewrite leb_spec, H1; auto with zarith. - assert (H1: (φ (m + n) = φ m + φ n)%Z). { rewrite add_spec, Zmod_small; auto with zarith. } replace (n <=? m + n)%uint63 with true; auto. apply sym_equal; rewrite leb_spec, H1; auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63