proposition: Lemma demi_angle_centre: forall (A B C A' O : PO), triangle A B C -> O <> A' -> A' = milieu B C -> circonscrit O A B C -> double_AV (cons_AV (vec A B) (vec A C)) = double_AV (cons_AV (vec O A') (vec O C)).
proof: Proof. intros. deroule_triangle A B C. deroule_circonscrit A B C O. assert (double_AV (cons_AV (vec A B) (vec A C)) = cons_AV (vec O B) (vec O C)). apply angle_inscrit; auto. rewrite H10. assert (double_AV (cons_AV (vec O A') (vec O C)) = cons_AV (vec O B) (vec O C)). unfold double_AV. replace (cons_AV (vec O B) (vec O C)) with (plus (cons_AV (vec O B) (vec O A')) (cons_AV (vec O A') (vec O C))). assert (cons_AV (vec O B) (vec O A') = cons_AV (vec O A') (vec O C)). apply isocele_mediane_bissectrice; auto. apply (circonscrit_isocele H2). rewrite H11; auto. apply Chasles; auto. rewrite H11; auto. Qed.