proposition: Lemma C_RInt_segm_swap (f : C -> C) (z1 z2 : C) : - C_RInt_segm f z1 z2 = C_RInt_segm f z2 z1.
proof: Proof. unfold C_RInt_segm. generalize (opp_mult_l (z2 - z1) (C_RInt (fun t : R => f (scal (1 - t)%R z1 + scal t z2)) 0 1)). rewrite /opp /mult /=. move => /= ->. apply f_equal2. apply Copp_minus_distr. rewrite (C_RInt_ext (fun t : R => opp ((-1) * (f (scal (1 - (-1 * t + 1)%R)%R z2 + scal (-1 * t + 1)%R z1)%C)))). rewrite C_RInt_opp. rewrite C_RInt_swap. rewrite (C_RInt_comp_lin (fun t : R => f (scal (1 - t)%R z2 + scal t z1)) (-1) (1) 1 0) ; apply f_equal2 ; ring. intros x _ ; simpl. apply injective_projections ; simpl ; ring_simplify ; apply f_equal ; apply f_equal ; apply injective_projections ; rewrite /= /scal /= /mult /= ; ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)