How to use a lemma that is defined in a Coq Importing Lemma from standard library module defined as `Module Type ?? (Import ?? : ??) (Import ?? : ?? ??).`

improved formatting

Source Link

edited Apr 12 at 11:59

How can I use the Lemma div_0_lLemma div_0_l from the standard library? Somehow I cannot instantiate the module that is defined as

Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).

How can I use the Lemma div_0_l from the standard library? Somehow I cannot instantiate the module that is defined as

Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).

How can I use the Lemma div_0_l from the standard library? Somehow I cannot instantiate the module that is defined as

Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).

Source Link

asked Apr 7 at 16:19

Coq Importing Lemma from standard library module defined as `Module Type ?? (Import ?? : ??) (Import ?? : ?? ??).`

How can I use the Lemma div_0_l from the standard library? Somehow I cannot instantiate the module that is defined as

Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).

coq