proposition: Fact rem_2_bool2nat b n : rem (bool2nat b+2*n) 2 = bool2nat b.
proof: Proof. destruct b; unfold bool2nat. + apply rem_2_fix_2. + apply rem_2_fix_1. 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)