proposition: Lemma NUMPAIR_INJ : forall x1 : nat, forall y1 : nat, forall x2 : nat, forall y2 : nat, ((NUMPAIR x1 y1) = (NUMPAIR x2 y2)) = ((x1 = x2) /\ (y1 = y2)).
proof: Proof. intros x1 y1 x2 y2. apply prop_ext. 2: intros [e1 e2]; subst; reflexivity. unfold NUMPAIR, NUMERAL, BIT1, BIT0. intro e. destruct (Compare_dec.lt_eq_lt_dec x1 x2) as [[h|h]|h]. apply False_rec. destruct (ge_is_add h) as [k hk]. subst x2. generalize (f_equal (fun x => div x (2 ^ x1)) e). rewrite DIV_MULT, pow_add, pow_succ_r, (mul_comm 2 (2 ^ x1)), <- !mul_assoc, DIV_MULT. lia. apply pow_nonzero. lia. lia. apply pow_nonzero. lia. subst x2. split. reflexivity. generalize (f_equal (fun x => div x (2 ^ x1)) e). rewrite !DIV_MULT. lia. apply pow_nonzero. lia. apply pow_nonzero. lia. apply False_rec. destruct (ge_is_add h) as [k hk]. subst x1. generalize (f_equal (fun x => div x (2 ^ x2)) e). rewrite DIV_MULT, pow_add, pow_succ_r, (mul_comm 2 (2 ^ x2)), <- !mul_assoc, DIV_MULT. lia. apply pow_nonzero. lia. lia. apply pow_nonzero. lia. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat