proposition: Lemma lsl_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%uint63.
proof: Proof. apply to_Z_inj; rewrite -> !lsl_spec, !add_spec, Zmult_mod_idemp_l. rewrite -> !lsl_spec, <-Zplus_mod. apply (f_equal2 Z.modulo); auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63