proposition: Lemma R_complete_ax2 : forall F1 F2 : (R -> Prop) -> Prop, filter_le F1 F2 -> filter_le F2 F1 -> R_complete_lim F1 = R_complete_lim F2.
proof: Proof. intros F1 F2 H12 H21. unfold R_complete_lim. apply f_equal, Lub_Rbar_eqset. split. apply H21. apply H12. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub