diff --git a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean index 6f39832..207788c 100644 --- a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean +++ b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean @@ -38,7 +38,7 @@ to the context, because you just supplied the proof of it (`succ_inj a b`). ## Example If you have a proof to hand, then you don't even need to state what you -are proving. example +are proving. For example `have h2 := succ_inj a b`