proposition: Fact nat_meet_12n n : 1⇣(2*n) = 0.
proof: Proof. replace 1 with (1+0*power 1 2) at 1 by auto. replace (2*n) with (0+n*power 1 2) by (rewrite power_1; ring). rewrite nat_meet_euclid_power_2; rewrite power_1; try lia. rewrite nat_meet_0n, nat_meet_n0; 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)