proposition: Lemma nat_tup_eta n : nat_tup (nat_fst n) (nat_snd n) = n.
proof: Proof. forward eapply invert_nat_fun_sat2 with (f := arith_sum) (y := n) as X. rewrite arith_sum_0, arith_sum_S; ins; lia. rewrite arith_sum_S in *; unfold nat_tup. replace (nat_fst n + nat_snd n) with (invert_nat_fun arith_sum n). all: unfold nat_fst, nat_snd; lia. Qed.
imports: NPeano Arith micromega.Lia Setoid HahnBase