Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/SsreflectTutorial_3.4_edivnP_right.v

Created July 26, 2014 06:02
Show Gist options
  • Save yoshihiro503/0d614df5bcf6840e6541 to your computer and use it in GitHub Desktop.
Save yoshihiro503/0d614df5bcf6840e6541 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
SsreflectTutorial_3.4_edivnP_right.v
Lemma edivnP_right : forall m d, edivn_spec_right m d (edivn m d).
Proof.
Check edivnP.
move=> m d.
case: (edivnP m d) => q r eq_m_dqr impl_0d_rd.
by apply: EdivnSpec_right.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment