We start with Paeno numbers because they are probably the simplest inductive data type that set the scene for how we tend to proves things in dependently typed programming (inductive reasoning). Proving the things you want are probably doable (I can't say for certain, they are vaguely specified which does not fit with formal methods), but significantly more involved. Trying to take the reader from nothing to that in a single blog post or talk is beyond anyone's ability. Generally, this is because dependent types aren't quite ready for mainstream in terms of convenience.

That said, I'd read some of Edwin Brady's research, as he is actively trying to find the intersection of "business programming" and dependent types: https://edwinb.wordpress.com/publications/