(** {2 Fermat's little theorem for n = 3} *) use int.Int use int.Power (* lemma power_0_left : forall n. power 0 n = 0 lemma power_3 : forall x. x >= 1 -> power (x-1) 3 = power x 3 - 3 * x * x + 3 * x - 1 *) let rec ghost little_fermat_3 (x : int) : int requires { x >= 0 } variant { ? } ensures { power x 3 - x = 3 * result } = ? let lemma lem_little_fermat_3 (x : int) requires { x >= 0 } ensures { exists y. power x 3 - x = 3 * y } = ?