proposition: Lemma nat_join_euclid2 q r1 d1 r2 d2 : r1 < power q 2 -> r2 < power q 2 -> (r1+d1*power q 2) ⇡ (r2+d2*power q 2) = (r1⇡r2) + (d1⇡d2)*power q 2.
proof: Proof. unfold nat_join. intros H1 H2. do 2 (rewrite nat_euclid_pow2_lb; auto). rewrite <- lb_nat_shift, <- lb_plus_spec_0. apply lb_mask_equiv_equal. rewrite lb_ortho_plus_join. 2: apply lb_shift_ortho, lb_join_length_le; apply nat_lb_length; auto. rewrite lb_shift_join. rewrite lb_join_assoc, <- (lb_join_assoc ⟬ r1 ⟭). rewrite (lb_join_comm _ ⟬ r2 ⟭). repeat rewrite lb_join_assoc; auto. Qed.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)