proposition: Lemma is_C_RInt_segm_swap (f : C -> C) (z1 z2 l : C) : is_C_RInt_segm f z2 z1 l -> is_C_RInt_segm f z1 z2 (-l).
proof: Proof. rewrite /is_C_RInt_segm => H. evar (k : C). replace (- l) with k. apply is_RInt_swap. apply is_RInt_ext with (fun t : R => scal (-1) ((z1 - z2) * f (scal (1 - (-1 * t + 1)%R)%R z2 + scal (-1 * t + 1)%R z1)%C)). move => x _. replace (scal (1 - (-1 * x + 1)%R)%R z2 + scal (-1 * x + 1)%R z1) with (scal (1 - x)%R z1 + scal x z2). 2 : apply injective_projections ; rewrite /= /scal /= /mult /= ; ring. rewrite scal_opp_one. change opp with Copp. change eq with (@eq C). field. apply (is_RInt_comp_lin (fun t : R => (z1 - z2) * f (scal (1 - t)%R z2 + scal t z1)) (-1)%R (1)%R 1 0). ring_simplify (-1 * 1 + 1)%R (-1 * 0 + 1)%R. apply H. by []. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)