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