proposition: Lemma nat_meet_euclid_power_2 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_meet. 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_meet_length_le; apply nat_lb_length; auto. rewrite lb_shift_meet. rewrite lb_meet_join_distr. do 2 rewrite (lb_meet_comm (_↑_)). do 2 rewrite lb_meet_join_distr. rewrite lb_shift_ortho_meet; try (apply nat_lb_length; auto; fail). rew lb. rewrite (lb_meet_comm (lb_shift _ _)). rewrite lb_shift_ortho_meet; try (apply nat_lb_length; auto; fail). rew lb. rewrite lb_meet_comm. rewrite (lb_meet_comm (lb_shift _ _)); 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)