Shortest chain between the same point is of zero length
Use a more directly proved pp-len-even etc.
Fix a bug in usage of A-pt#eq
Define rho between two points

Prove that when e f are points, lambda e f is even and then define rho
Use divide definition in Data.Nat for rho