fact: Fixpoint rpeg {n : nat} := if n is n1.+1 return configuration 3 n -> peg 3 -> seq (configuration 3 n) then fun c p => let p1 := c ldisk in if p1 == p then [seq ↑[i]_p | i <- rpeg ↓[c] p] else let p2 := `p[p1, p] in [seq ↑[i]_p1 | i <- rpeg ↓[c] p2] ++ [seq ↑[i]_p | i <- `c[p2] :: ppeg p2 p] else fun _ _ => [::].
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)