proposition: Lemma BIT0_is_double : BIT0 = Nat.double.
proof: Proof. apply fun_ext; intro n. induction n; simpl. reflexivity. rewrite IHn. unfold Nat.double. simpl. rewrite PeanoNat.Nat.add_succ_r. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat