proposition: Lemma plength_aux_spec l p : Pos.to_nat (plength_aux l p) = length l + Pos.to_nat p.
proof: Proof. revert p. induction l; trivial. simpl plength_aux. intros. now rewrite IHl, Pos2Nat.inj_succ, Nat.add_succ_r. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat