fact: Definition next (s : state) := match s with | mks round a b (S c) => mks (S round) a b c | mks round a (S b) 0 => mks (S round) a b (S round) | mks round (S a) 0 0 => mks (S round) a (S round) 0 | _ => s end.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)