https://github.com/math-comp/analysis/blob/af08f5e9a149993baf055b8577020fef56f001ce/classical/boolp.v#L16 Compnent
analysis/classical/boolp.v
Line 16 in af08f5e
Compnent