proposition: Lemma restr_bin_fun_strext : forall (X : CPsMetricSpace) (P : cms_crr X -> CProp) (f : CSetoid_bin_fun X X IR), bin_fun_strext (Build_SubCSetoid X P) (Build_SubCSetoid X P) IR (restr_bin_fun P f).
proof: Proof. intros X P f. red in |- *. intros x1 x2 y1 y2. case y2. case y1. case x2. case x1. do 8 intro. intro H. exact (csbf_strext _ _ _ f _ _ _ _ H). Qed.
imports: CoRN.metrics.IR_CPMSpace