proposition: Lemma nat_meet_euclid_2 r1 d1 r2 d2 : r1 < 2 -> r2 < 2 -> (r1+2*d1) ⇣ (r2+2*d2) = (r1⇣r2) + 2*(d1⇣d2).
proof: Proof. intros H1 H2. do 3 rewrite (Nat.mul_comm 2). apply nat_meet_euclid_power_2 with (q := 1); 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)