More than 5 years have passed since last update.
RequireImportArith.TheoremTh1:forall(n:nat),(existsm:nat,n=m*2)->existsk:nat,n*2=k*4.Proof.intros.destructH.existsx.rewriteH.rewritemult_assoc_reverse.simpl.reflexivity.Qed.Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme