proposition: Lemma det_sum (p : Plane) (n : nat) (f : 'I_n -> Plane) : det 0 p (\sum_(i < n) f i) = \sum_(i < n) det 0 p (f i).
proof: Proof. elim: n f. by move=>f; rewrite 2!big_ord0 -det_cyclique det_alternate. move=>n IHn f. by rewrite 2!big_ord_recl detD IHn. Qed.
imports: encompass conv mathcomp(all_ssreflect all_algebra vector reals normedtype) mathcomp(classical_sets boolp mathcomp_extra) counterclockwise mathcomp.algebra_tactics(ring) mathcomp.zify(zify)