proposition: Lemma sum_diff_diff : forall O E E' AX BX CX AXMBX AXMCX BXMCX, Diff O E E' AX BX AXMBX -> Diff O E E' AX CX AXMCX -> Diff O E E' BX CX BXMCX -> Sum O E E' AXMBX BXMCX AXMCX.
proof: Proof. intros O E E' AX BX CX AXMBX AXMCX BXMCX HAXMBX HAXMCX HBXMCX. assert (HNC : ~ Col O E E') by (unfold Diff, Sum, Ar2 in *; destruct HAXMBX; spliter; auto). assert (HColAX : Col O E AX) by (unfold Diff, Sum, Ar2 in *; destruct HAXMBX; spliter; auto). assert (HColBX : Col O E BX) by (unfold Diff, Sum, Ar2 in *; destruct HBXMCX; spliter; auto). assert (HColCX : Col O E CX) by (unfold Diff, Opp, Sum, Ar2 in *; destruct HBXMCX; spliter; auto). assert (HColAXMBX : Col O E AXMBX) by (unfold Diff, Sum, Ar2 in *; destruct HAXMBX; spliter; auto). assert (HColAXMCX : Col O E AXMCX) by (unfold Diff, Sum, Ar2 in *; destruct HAXMCX; spliter; auto). assert (HColBXMCX : Col O E BXMCX) by (unfold Diff, Sum, Ar2 in *; destruct HBXMCX; spliter; auto). destruct (opp_exists O E E' HNC BX) as [MBX HMBX]; Col. assert (HSum1 : Sum O E E' AX MBX AXMBX). { apply diff_sum in HAXMBX; apply sum_assoc_1 with AXMBX BX O; apply sum_comm; auto; apply sum_O_B; Col. } destruct (opp_exists O E E' HNC CX) as [MCX HMCX]; Col. assert (HSum2 : Sum O E E' BX MCX BXMCX). { apply diff_sum in HBXMCX; apply sum_assoc_1 with BXMCX CX O; apply sum_comm; auto; apply sum_O_B; Col. } apply sum_assoc_1 with AX MBX MCX; auto. { apply sum_assoc_2 with BX MCX O; auto; apply sum_O_B; Col. unfold Opp, Sum, Ar2 in *; spliter; Col. } { apply diff_sum in HAXMCX; apply sum_assoc_1 with AXMCX CX O; apply sum_comm; auto; apply sum_O_B; Col. } Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg