proposition: Lemma decode_encode_nat `{Countable A} (x : A) : decode_nat (encode_nat x) = Some x.
proof: Proof. pose proof (Pos2Nat.is_pos (encode x)). unfold decode_nat, encode_nat. rewrite Nat.succ_pred by lia. by rewrite Pos2Nat.id, decode_encode. Qed.
imports: Coq.QArith(QArith_base Qcanon) stdpp(well_founded) stdpp(options)