proposition: Lemma is_C_RInt_segm_Chasles (f : C -> C) (z1 z2 z3 : C) l1 l2 : complex_line z1 z3 z2 -> is_C_RInt_segm f z1 z2 l1 -> is_C_RInt_segm f z2 z3 l2 -> is_C_RInt_segm f z1 z3 (plus l1 l2).
proof: Proof. rewrite /is_C_RInt_segm ; case => p -> H1 H2. case: (Req_dec p 0) => Hp0. rewrite Hp0 in H1 H2 => {p Hp0}. apply (is_RInt_ext _ (fun t : R => (z3 - z1) * f (scal (1 - t)%R z1 + scal t z3))) in H2. Focus 2. move => x _. by rewrite scal_zero_l Rminus_0_r scal_one Cplus_0_r. apply (is_RInt_ext _ (fun _ => zero)) in H1. Focus 2. move => x _ ; simpl. by rewrite scal_zero_l Rminus_0_r scal_one Cplus_0_r /Cminus Cplus_opp_r Cmult_0_l. move: (is_RInt_plus _ _ _ _ _ _ H1 H2). apply is_RInt_ext. now move => x _ ; rewrite plus_zero_l. case: (Req_dec 1 p) => Hp1. rewrite -Hp1 in H1 H2 => {p Hp1 Hp0}. apply (is_RInt_ext _ (fun t : R => (z3 - z1) * f (scal (1 - t)%R z1 + scal t z3))) in H1. Focus 2. move => x _. by rewrite Rminus_eq_0 scal_zero_l scal_one Cplus_0_l. apply (is_RInt_ext _ (fun _ => zero)) in H2. Focus 2. move => x _ ; simpl. by rewrite Rminus_eq_0 scal_zero_l scal_one Cplus_0_l /Cminus Cplus_opp_r Cmult_0_l. move: (is_RInt_plus _ _ _ _ _ _ H1 H2). apply is_RInt_ext. now move => x _ ; rewrite plus_zero_r. apply is_RInt_Chasles with p. eapply is_RInt_ext, (is_RInt_comp_lin _ (/ p) 0). 2: replace (/ p * 0 + 0)%R with 0 by ring. 2: replace (/ p * p + 0)%R with 1 by now field. 2: by apply H1. intros x _ ; simpl. rewrite !scal_R_Cmult !RtoC_minus !RtoC_plus !RtoC_mult !RtoC_inv //. rewrite Cmult_assoc. replace (/ p * ((1 - p) * z1 + p * z3 - z1)) with (z3 - z1). 2: now field ; contradict Hp0 ; injection Hp0. apply f_equal, f_equal. now field ; contradict Hp0 ; injection Hp0. apply Rminus_eq_contra in Hp1. eapply is_RInt_ext, (is_RInt_comp_lin _ (/ (1 - p)) (-p / (1 - p))). 2: replace (/ (1 - p) * p + - p / (1 - p))%R with 0 by now field. 2: replace (/ (1 - p) * 1 + - p / (1 - p))%R with 1 by now field. 2: by apply H2. intros x _ ; simpl. rewrite !scal_R_Cmult !RtoC_minus !RtoC_plus !RtoC_mult !RtoC_inv // !RtoC_opp !RtoC_minus. rewrite Cmult_assoc. replace (/ (1 - p) * (z3 - ((1 - p) * z1 + p * z3))) with (z3 - z1). 2: now field ; contradict Hp0 ; injection Hp0. apply f_equal, f_equal. now field ; contradict Hp0 ; injection Hp0. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)