proposition: Fact bool2nat2bool : forall x, x < 2 -> bool2nat (nat2bool x) = x.
proof: Proof. intros [ | [ | ] ] ?; simpl; lia. 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)