fact: Fixpoint size_rpeg {n : nat} : (configuration _ n) -> _ -> nat := match n with | 0 => fun _ _ => 0 | n1.+1 => fun c p => let p1 := c ldisk in if p1 == p then size_rpeg ↓[c] p else let p2 := `p[p1, p] in size_rpeg ↓[c] p2 + 2 ^ n1 end.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)