forall m n : nat, m * n = (2 * m * n)%nat
     : Prop