proposition: Lemma add_pos_natE p n : add_pos_nat p n = Pos.to_nat p + n.
proof: Proof. elim: p n => //= p IHp n; rewrite !IHp; lia. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)