mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
3 lines
87 B
Plaintext
3 lines
87 B
Plaintext
|
|
goal mult_po_4: forall a,b:int. a > 0 -> a % 2 = 1 -> b + (a / 2) * (2 * b) = a * b
|