fact: Definition extend (t: T): CR := match decide (P t) with | left H => f (exist _ _ H) | right _ => 0 end.
imports: Unicode.Utf8 Program CRArith CRabs Qminmax Qauto Qround Qmetric stdlib_omissions.P stdlib_omissions.Z stdlib_omissions.Q stdlib_omissions.N metric2.Classified util.Container Ranges decision