13 lines
278 B
Text
13 lines
278 B
Text
|
import algebra.ordered_field
|
||
|
|
open algebra
|
||
|
|
section sequence_c
|
||
|
|
|
||
|
|
parameter Q : Type
|
||
|
|
parameter lof_Q : linear_ordered_field Q
|
||
|
|
definition to_lof [instance] : linear_ordered_field Q := lof_Q
|
||
|
|
include to_lof
|
||
|
|
|
||
|
|
theorem foo (a b : Q) : a + b = b + a := !add.comm
|
||
|
|
|
||
|
|
end sequence_c
|