diff options
| author | Jasper Hugunin | 2020-09-09 10:46:15 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | 8710a9437442003681e838a36ae572b7b24a958e (patch) | |
| tree | 2254ec3180b22a95895ef5248e43fd5d40a73c8f | |
| parent | 13a9a7f16acb520b1e38aeac9480f7d298a62bc7 (diff) | |
Modify Numbers/Natural/Abstract/NLcm.v to compile with -mangle-names
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NLcm.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v index 3a9cf34b25..b75b4521df 100644 --- a/theories/Numbers/Natural/Abstract/NLcm.v +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -169,7 +169,7 @@ Qed. Lemma lcm_divide_iff : forall n m p, (lcm n m | p) <-> (n | p) /\ (m | p). Proof. - intros. split. split. + intros n m p. split. split. transitivity (lcm n m); trivial using divide_lcm_l. transitivity (lcm n m); trivial using divide_lcm_r. intros (H,H'). now apply lcm_least. |